PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 16

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
Wyszukiwano:
w słowach kluczowych:  bisimulation
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote Resource Bisimilarity in Petri Nets is Decidable
Lomazova Irina, Bashkin Vladimir, Jančar Petr
Fundamenta Informaticae
|
2022
|
Vol. 186, nr 1-4
175--194
EN
Petri nets are a popular formalism for modeling and analyzing distributed systems. Tokens in Petri net models can represent the control flow state or resources produced/consumed by transition firings. We define a resource as a part (a submultiset) of Petri net markings and call two resources equivalent when replacing one of them with another in any marking does not change the observable Petri net behavior. We consider resource similarity and resource bisimilarity, two congruent restrictions of bisimulation equivalence on Petri net markings. Previously it was proved that resource similarity (the largest congruence included in bisimulation equivalence) is undecidable. Here we present an algorithm for checking resource bisimilarity, thereby proving that this relation (the largest congruence included in bisimulation equivalence that is a bisimulation) is decidable. We also give an example of two resources in a Petri net that are similar but not bisimilar.
2
Content available remote Modal Equivalence and Bisimilarity in Many-valued Modal Logics with Many-valued Accessibility Relations
Diaconescu Denisa
Fundamenta Informaticae
|
2020
|
Vol. 173, nr 2-3
177--189
EN
In this paper we investigate the Hennessy-Milner property for models of many-valued modal logics defined based on complete MTL-chains having many-valued accessibility relations. Our main result gives a necessary and sufficient algebraic condition for the class of image-finite models for such modal logics to admit the Hennessy-Milner property.
3
Content available remote Computing Bisimulation-Based Comparisons
Nguyen L. A.
Fundamenta Informaticae
|
2018
|
Vol. 157, nr 4
385--401
EN
We provide the first algorithm with a polynomial time complexity, O((m + n)2n2), for computing the largest bisimulation-based auto-comparison of a labeled graph in the setting with counting successors, where m is the number of edges and n is the number of vertices. This setting is like the case with graded modalities in modal logics and qualified number restrictions in description logics. Furthermore, by using the idea of Henzinger et al. for computing simulations, we give an efficient algorithm, with complexity O((m + n)n), for computing the largest bisimulation-based auto-comparison and the directed similarity relation of a labeled graph in the setting without counting successors. We also adapt our former algorithm for computing the simulation pre-order of a labeled graph in the setting with counting successors.
4
Content available remote Zestawienie i porównanie automatów probabilistycznych i kwantowych
Siedlecka-Lamch O.
Studia i Materiały / Europejska Uczelnia Informatyczno-Ekonomiczna w Warszawie
|
2017
|
Nr 1(13)
77--83
PL
Większość systemów informatycznych można modelować z wykorzystaniem różnego rodzaju automatów skończonych: deterministycznych, niedeterministycznych, probabilistycznych itp. Automaty te można badać pod kątem osiągalności określonych stanów i dzięki temu sprawdzać, czy system może znaleźć się w stanie krytycznym, błędnym, niechcianym. Mamy również możliwość dokonania operacji minimalizacji automatów. Praktycznie ogranicza się to do znalezienia stanów nadmiarowych i nieosiągalnych – dzięki czemu mamy również sposobność zminimalizować oryginalny, modelowany system, zaoszczędzić na dokonywanych operacjach, pamięci, a nawet sprzęcie.
EN
Most IT systems can be modeled with the use of various types of finite automata: deterministic, non-deterministic, probabilistic, etc. These automatons can be tested for reachability of certain states and thus we can check whether the system can be in a critical, erroneous or unwanted state. We also have the ability to perform the operation of automata minimization. Practically, this is limited to finding redundant and unreachable states – so we also have the opportunity to minimize the original, modeled system, save on operations amount, memory, and even hardware.
5
Content available remote True Concurrent Equivalences in Time Petri Nets
Virbitskaite I., Bushin D., Best E.
Fundamenta Informaticae
|
2016
|
Vol. 149, nr 4
401--418
EN
The intention of the paper is towards a framework for developing, studying and comparing observational equivalences in the setting of a real-time true concurrent model. In particular, we introduce a family of trace and bisimulation equivalences in interleaving, step, partial order and causal net semantics in the setting of time Petri nets (elementary net systems whose transitions are labeled with time firing intervals, can fire only if their lower time bounds are attained, and are forced to fire when their upper time bounds are reached) [3]. We deal with the relationships between the equivalences showing the discriminating power of the approaches of the linear-time - branching-time and interleaving - partial order spectra and construct a hierarchy of equivalent classes of time Petri nets. This allows studying in complete detail the timing behaviour in addition to the degrees of relative concurrency and nondeterminism of processes.
6
Content available remote Bisimulation Cuts For Structuring Markov Transition Systems
Doberkat E.-E.
Fundamenta Informaticae
|
2016
|
Vol. 149, nr 4
363--383
EN
In Universal Algebra the structure of congruences for algebraic systems is fairly well investigated, and the relationship to the structure of the underlying system proper is well known. We propose a first step into this direction for studying the structure of congruences for stochastic relations. A Galois connection to a certain class of Boolean σ-algebras is exploited, atoms and antiatoms are identified, and it is show that a σ-basis exists. These constructions are applied to the problem of finding bisimulation cuts of a congruence. It cuts the relation through a span of morphisms with a minimum of joint events.
7
Content available remote Mapping Sets and Hypersets into Numbers
D’Agostino G., Omodeo E. G., Policriti A., Tomescu A. I.
Fundamenta Informaticae
|
2015
|
Vol. 140, nr 3/4
307--328
EN
We introduce and prove the basic properties of encodings that generalize to non-wellfounded hereditarily finite sets the bijection defined by Ackermann in 1937 between hereditarily finite sets and natural numbers.
8
Content available Dynamic network functional comparison via approximate-bisimulation
Donnarumma F., Murano A., Prevete R.
Control and Cybernetics
|
2015
|
Vol. 44, no. 1
99--127
EN
It is generally unknown how to formally determine whether different neural networks have a similar behaviour. This question intimately relates to the problem of finding a suitable similarity measure to identify bounds on the input-output response distances of neural networks, which has several interesting theoretical and computational implications. For example, it can allow one to speed up the learning processes by restricting the network parameter space, or to test the robustness of a network with respect to parameter variation. In this paper we develop a procedure that allows for comparing neural structures among them. In particular, we consider dynamic networks composed of neural units, characterised by non-linear differential equations, described in terms of autonomous continuous dynamic systems. The comparison is established by importing and adapting from the formal verification setting the concept of δ−approximate bisimulations techniques for non-linear systems. We have positively tested the proposed approach over continuous time recurrent neural networks (CTRNNs).
9
Content available remote Bisimulation-Based Concept Learning in Description Logics
Tran T.-L., Ha Q.-T., Hoang T.-L.-G., Nguyen L. A., Nguyen H. S.
Fundamenta Informaticae
|
2014
|
Vol. 133, nr 2/3
287--303
EN
Concept learning in description logics (DLs) is similar to binary classification in traditional machine learning. The difference is that in DLs objects are described not only by attributes but also by binary relationships between objects. In this paper, we develop the first bisimulation-based method of concept learning in DLs for the following setting: given a knowledge base KB in a DL, a set of objects standing for positive examples and a set of objects standing for negative examples, learn a concept C in that DL such that the positive examples are instances of C w.r.t. KB, while the negative examples are not instances of C w.r.t. KB. We also prove soundness of our method and investigate its C-learnability.
10
Content available remote Unifying Equivalences for Higher Dimensional Automata
Oshevskaya E., Virbitskaite I., Best E.
Fundamenta Informaticae
|
2012
|
Vol. 119, nr 3/4
357-372
EN
The intention of the paper is to show how several categorical (open morphisms, path mor- phisms and coalgebraic morphisms based) approaches to an abstract characterization of bisimulation relate to each other and to behavioral bisimulations, in the setting of higher dimensional automata. Such a relating makes it possible to develop a metatheory designed for unified definition and study of equivalences in true concurrency semantics.
11
Content available remote Bisimulation Minimisation of Weighted Automata on Unranked Trees
Högberg J., Maletti A.
Fundamenta Informaticae
|
2009
|
Vol. 92, nr 1-2
103-130
EN
Several models of automata are available that operate unranked trees. Two well-known examples are the stepwise unranked tree automaton (suta) and the parallel unranked tree automaton (puta). By adding a weight, taken from some semiring, to every transition we generalise these two qualitative automata models to quantitative models, thereby obtaining weighted stepwise unranked tree automata (wsuta) and weighted parallel unranked tree automata (wputa); the qualitative automata models are reobtained by choosing the BOOLEAN semiring. The weighted versions have applications in natural language processing, XML-based data management and quantitative information retrieval. We address the minimisation problem of wsuta and wputa by using (forward and backward) bisimulations and we prove the following results: (1) for every wsuta an equivalent forward (resp. backward) bisimulation minimal wsuta can be computed in time O(mn) where n is the number of states and m is the number of transitions of the given wsuta; (2) the same result is proved for wputa instead of wsuta; (3) if the semiring is additive cancellative or the BOOLEAN semiring, then the bound can be improved to O(mlog n) for both wsuta and wputa; (4) for every deterministic puta we can compute a minimal equivalent deterministic puta in time O(mlog n); (5) the automata models wsuta, wputa, and weighted unranked tree automaton have the same computational power.
12
Content available remote A Relation-Algebraic Theory of Bisimulations
Winter M.
Fundamenta Informaticae
|
2008
|
Vol. 83, nr 4
429-449
EN
In this paper we develop an algebraic/categorical theory of bisimulations using relational methods. We define a general notion, which is capable of handeling different version of bisimilarity in a common context. Furthermore, the approach relates bisimulations with the notion of a covering known from the theory of graphs and their applications in topology and complex analysis.
13
Content available remote On Designated Values in Multi-Valued CTLS* Model Checking
Konikowska B., Penczek W.
Fundamenta Informaticae
|
2004
|
Vol. 60, nr 1-4
211--224
EN
A multi-valued version of CTLS* (mv-CTLS*), where both the propositions and the accessibility relation are multi-valued, taking values in a complete lattice with a complement, is considered. Contrary to all the existing model checking results for multi-valued modal logics, our lattices are not required to be finite. A set of restrictions is provided under which there is a direct translation from mv-CTLS* to CTLS* model checking problem for designated values. Bisimulation induced by mv-CTLS* is characterized.
14
Content available remote Zastosowanie algebry procesów do wspomagania projektowania poprawnego oprogramowania systemów reaktywnych
Szmuc T., Oskwarek S.
Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
|
2001
|
T. 5, z. 1/2
523-533
PL
W pracy pokazano możliwość wspomagania analizy poprawności oprogramowania systemów reaktywnych. Pokazano translację między specyfikacją systemu w języku SDL (FSM) a algebrą procesów CCS oraz opisano koncepcję dowodzenia poprawności (bisymulacji). Rozważania prowadzone są na znanym w literaturze przykładzie systemu obronnego krążownika rakietowego.
EN
An application of process algebra (CCS) supporting design of correct software for reactive systems is presented in the paper. A translation between SDL (FSM) diagrams and process algebra is shown and a concept of correctness (bisimulation) proving is given. All the considerations are carried out using well-known Naval Vessel problem.
15
Content available remote Analysis of timed concurrent models based on testing equivalence
Andreeva M.V., Bozhenkova E.N., Virbitskaite I.B.
Fundamenta Informaticae
|
2000
|
Vol. 43, Nr 1-4
1-20
EN
The intention of the paper is to extend the testing methodology to a model of event structures with a dense time domain. Alternative characterizations of timed testing re-lations are provided. We also present algorithms for deciding timed testing for a sub-class of the model under consideration. The key to our decision algorithms is that timed testing equivalences can be reduced to appropriate symbolic bisimulations.
16
Content available remote Bisimulation and open maps for timed transition systems
Nielsen M., Hune T.
Fundamenta Informaticae
|
1999
|
Vol. 38, Nr 1,2
61-77
EN
Formal models for real-time systems have been studied intensively over the past decade. Much of the theory of untimed systems have been lifted to real-time settings. One example is the notion of bisimulation applied to timed transition systems, which is studied here within the general categorical framework of open maps. We define a category of timed transition systems, and show how to characterize standard timed bisimulation in terms of spans of open maps with a natural choice of a path category. This allows us to apply general results from the theory of open maps, e.g. the existence of canonical models and characteristic logics. Also, we obtain here an alternative proof of decidability of bisimulation for finite transition sys-tems, and illustrate the use of open maps in finite presentations of bisimulations.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.