The Experts below are selected from a list of 20229 Experts worldwide ranked by ideXlab platform
Zining Cao - One of the best experts on this subject based on the ideXlab platform.
-
More on Bisimulations for higher order π-calculus
Theoretical Computer Science, 2012Co-Authors: Zining CaoAbstract:In this paper, we prove the coincidence between strong/weak context Bisimulation and strong/weak normal Bisimulation for higher order @p-calculus, which generalizes Sangiorgi's work. To achieve this aim, we introduce indexed higher order @p-calculus, which is similar to higher order @p-calculus except that every prefix of any process is assigned indices. Furthermore we present corresponding indexed Bisimulations for this calculus, and prove the equivalence between these indexed Bisimulations. Based on this result, we prove the main result of this paper, i.e., the equivalence between strong/weak context Bisimulation and strong/weak normal Bisimulation.
-
Branching Bisimulations for Higher Order p-Calculus
2009 International Conference on Information Technology and Computer Science, 2009Co-Authors: Zining CaoAbstract:In this paper, we introduce branching context Bisimulation, branching normal Bisimulation and branching barbed congruence for higher order πcalculus. Moreover we prove the equivalence of the three branching Bisimulations. At last, we compare branching context Bisimulations with other Bisimulations for higher orderπ-calculus.
-
ASIAN - A spatial logical characterisation of context Bisimulation
Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 2007Co-Authors: Zining CaoAbstract:In this paper, we present a spatial logic for higher order π-calculus. In order to prove that the induced logical equivalence coincides with context Bisimulation, we present some new Bisimulations, and prove the equivalence between these new Bisimulations and context Bisimulation. Furthermore, we present a variant of this spatial logic and prove that it also provides a logical characterisation of context Bisimulation.
-
TAMC - A logic for distributed higher order π-calculus
Lecture Notes in Computer Science, 1Co-Authors: Zining CaoAbstract:In this paper, we present a spatial logic for distributed higher order π-calculus. In order to prove that the induced logical equivalence coincides with distributed context Bisimulation, we present some new Bisimulations, and prove the equivalence between these new Bisimulations and distributed context Bisimulation. Furthermore, we present a variant of this spatial logic and prove that it gives a logical characterisation of distributed Bisimulations.
Milan Bašić - One of the best experts on this subject based on the ideXlab platform.
-
Nondeterministic automata: Equivalence, Bisimulations, and uniform relations
Information Sciences, 2014Co-Authors: Miroslav Irić, Jelena Ignjatović, Milan Bašić, Ivana JančićAbstract:In this paper we study the equivalence of nondeterministic automata pairing the concept of a Bisimulation with the recently introduced concept of a uniform relation. In this symbiosis, uniform relations serve as equivalence relations which relate states of two possibly different nondeterministic automata, and Bisimulations ensure compatibility with the transitions, initial and terminal states of these automata. We define six types of Bisimulations, but due to the duality we discuss three of them: forward, backward-forward, and weak forward Bisimulations. For each of these three types of Bisimulations we provide a procedure which decides whether there is a Bisimulation of this type between two automata, and when it exists, the same procedure computes the greatest one. We also show that there is a uniform forward Bisimulation between two automata if and only if the factor automata with respect to the greatest forward Bisimulation equivalences on these automata are isomorphic. We prove a similar theorem for weak forward Bisimulations, using the concept of a weak forward isomorphism instead of an isomorphism. We also give examples that explain the relationships between the considered types of Bisimulations.
-
Bisimulations for fuzzy automata
Fuzzy Sets and Systems, 2012Co-Authors: Miroslav Ćirić, Jelena Ignjatović, Nada Damljanović, Milan BašićAbstract:Bisimulations have been widely used in many areas of computer science to model equivalence between various systems, and to reduce the number of states of these systems, whereas uniform fuzzy relations have recently been introduced as a means to model the fuzzy equivalence between elements of two possible different sets. Here we use the conjunction of these two concepts as a powerful tool in the study of equivalence between fuzzy automata. We prove that a uniform fuzzy relation between fuzzy automata A and B is a forward Bisimulation if and only if its kernel and co-kernel are forward Bisimulation fuzzy equivalence relations on A and B and there is a special isomorphism between factor fuzzy automata with respect to these fuzzy equivalence relations. As a consequence we get that fuzzy automata A and B are UFB-equivalent, i.e., there is a uniform forward Bisimulation between them, if and only if there is a special isomorphism between the factor fuzzy automata of A and B with respect to their greatest forward Bisimulation fuzzy equivalence relations. This result reduces the problem of testing UFB-equivalence to the problem of testing isomorphism of fuzzy automata, which is closely related to the well-known graph isomorphism problem. We prove some similar results for backward-forward Bisimulations, and we point to fundamental differences. Because of the duality with the studied concepts, backward and forward-backward Bisimulations are not considered separately. Finally, we give a comprehensive overview of various concepts on deterministic, nondeterministic, fuzzy, and weighted automata, which are related to Bisimulations.
-
Bisimulations for fuzzy automata
arXiv: Formal Languages and Automata Theory, 2011Co-Authors: Miroslav Ćirić, Jelena Ignjatović, Nada Damljanović, Milan BašićAbstract:Bisimulations have been widely used in many areas of computer science to model equivalence between various systems, and to reduce the number of states of these systems, whereas uniform fuzzy relations have recently been introduced as a means to model the fuzzy equivalence between elements of two possible different sets. Here we use the conjunction of these two concepts as a powerful tool in the study of equivalence between fuzzy automata. We prove that a uniform fuzzy relation between fuzzy automata $\cal A$ and $\cal B$ is a forward Bisimulation if and only if its kernel and co-kernel are forward Bisimulation fuzzy equivalences on $\cal A$ and $\cal B$ and there is a special isomorphism between factor fuzzy automata with respect to these fuzzy equivalences. As a consequence we get that fuzzy automata $\cal A$ and $\cal B$ are UFB-equivalent, i.e., there is a uniform forward Bisimulation between them, if and only if there is a special isomorphism between the factor fuzzy automata of $\cal A$ and $\cal B$ with respect to their greatest forward Bisimulation fuzzy equivalences. This result reduces the problem of testing UFB-equivalence to the problem of testing isomorphism of fuzzy automata, which is closely related to the well-known graph isomorphism problem. We prove some similar results for backward-forward Bisimulations, and we point to fundamental differences. Because of the duality with the studied concepts, backward and forward-backward Bisimulations are not considered separately. Finally, we give a comprehensive overview of various concepts on deterministic, nondeterministic, fuzzy, and weighted automata, which are related to Bisimulations.
George J. Pappas - One of the best experts on this subject based on the ideXlab platform.
-
Approximate Bisimulation relations for constrained linear systems
Automatica, 2007Co-Authors: Antoine Girard, George J. PappasAbstract:In this paper, we define the notion of approximate Bisimulation relation between two continuous systems. While exact Bisimulation requires that the observations of two systems are and remain identical, approximate Bisimulation allows the observations to be different provided the distance between them remains bounded by some parameter called precision. Approximate Bisimulation relations are conveniently defined as level sets of a so-called Bisimulation function which can be characterized using Lyapunov-like differential inequalities. For a class of constrained linear systems, we develop computationally effective characterizations of Bisimulation functions that can be interpreted in terms of linear matrix inequalities and optimal values of static games. We derive a method to evaluate the precision of the approximate Bisimulation relation between a constrained linear system and its projection. This method has been implemented in a Matlab toolbox: MATISSE. An example of use of the toolbox in the context of safety verification is shown.
-
CTCS - Bisimulation Relations for Dynamical and Control Systems
Electronic Notes in Theoretical Computer Science, 2003Co-Authors: Esfandiar Haghverdi, Paulo Tabuada, George J. PappasAbstract:AbstractIn this paper we propose a new equivalence relation for dynamical and control systems called Bisimulation. As the name implies this definition is inspired by the fundamental notion of Bisimulation introduced by R. Milner for labeled transition systems. It is however, more subtle than its namesake in concurrency theory, mainly due to the fact that here, one deals with relations on manifolds. We further show that the Bisimulation relations for dynamical and control systems defined in this paper are captured by the notion of abstract Bisimulation of Joyal, Nielsen and Winskel (JNW). This result not only shows that our equivalence notion is on the right track, but also confirms that the abstract Bisimulation of JNW is general enough to capture equivalence notions in the domain of continuous systems. We believe that the unification of the Bisimulation relation for labeled transition systems and dynamical systems under the umbrella of abstract Bisimulation, as achieved in this work, is a first step towards a unified approach to modeling of and reasoning about the dynamics of discrete and continuous structures in computer science and control theory
-
Unifying Bisimulation relations for discrete and continuous systems
2002Co-Authors: Esfandiar Haghverdi, George J. PappasAbstract:The fundamental notion of Bisimulation has inspired various notions of system equivalences in concurrency theory. Many notions of Bisimulation for various discrete systems have been recently unified in the abstract category theoretical formulation of Bisimulation due to Joyal, Nielsen and Winskel. In this paper, we adopt their framework and unify the notions of Bisimulation equivalences for discrete, continuous dynamical and control systems. This shows that our equivalence notion is on the right track, but also confirms that abstract Bisimulation is general enough to capture equivalence notions in the domain of continuous systems. We believe that the unification of the Bisimulation relation for labelled transition systems and dynamical systems under the umbrella of abstract Bisimulation, as achieved in this work, is a first step towards a unified approach to modeling of and reasoning about the dynamics of discrete and continuous structures in computer science and control theory.
-
Approximate Bisimulations for Nonlinear Dynamical Systems
Proceedings of the 44th IEEE Conference on Decision and Control, 1Co-Authors: Antoine Girard, George J. PappasAbstract:The notion of exact Bisimulation equivalence for nondeterministic discrete systems has recently resulted in notions of exact Bisimulation equivalence for continuous and hybrid systems. In this paper, we establish the more robust notion of approximate Bisimulation equivalence for nondeterministic nonlinear systems. This is achieved by requiring that a distance between system observations starts and remains, close, in the presence of nondeterministic system evolution. We show that approximate Bisimulation relations can be characterized using a class of functions called Bisimulation functions. For nondeterministic nonlinear systems, we show that conditions for the existence of Bisimulation functions can be expressed in terms of Lyapunov-like inequalities, which for deterministic systems can be computed using recent sum-of-squares techniques. Our framework is illustrated on a safety verification example.
Jelena Ignjatović - One of the best experts on this subject based on the ideXlab platform.
-
IFSA-EUSFLAT - Bisimulations in fuzzy social network analysis
Proceedings of the 2015 Conference of the International Fuzzy Systems Association and the European Society for Fuzzy Logic and Technology, 2015Co-Authors: Jelena Ignjatović, Miroslav Ćirić, Ivan StankovicAbstract:In this paper we introduce two types of simulations and five types of Bisimulations for fuzzy social networks, and we study one of them – regular Bisimulations. We prove that if there exists at least one regular Bisimulation between two fuzzy networks, then there exists the greatest Bisimulation of this type, and we provide a procedure for testing the existence of a regular Bisimulation between two fuzzy networks, and computing the greatest one, whenever it exists. We also establish a natural relationship between regular Bisimulations and regular fuzzy equivalences.
-
Nondeterministic automata: Equivalence, Bisimulations, and uniform relations
Information Sciences, 2014Co-Authors: Miroslav Irić, Jelena Ignjatović, Milan Bašić, Ivana JančićAbstract:In this paper we study the equivalence of nondeterministic automata pairing the concept of a Bisimulation with the recently introduced concept of a uniform relation. In this symbiosis, uniform relations serve as equivalence relations which relate states of two possibly different nondeterministic automata, and Bisimulations ensure compatibility with the transitions, initial and terminal states of these automata. We define six types of Bisimulations, but due to the duality we discuss three of them: forward, backward-forward, and weak forward Bisimulations. For each of these three types of Bisimulations we provide a procedure which decides whether there is a Bisimulation of this type between two automata, and when it exists, the same procedure computes the greatest one. We also show that there is a uniform forward Bisimulation between two automata if and only if the factor automata with respect to the greatest forward Bisimulation equivalences on these automata are isomorphic. We prove a similar theorem for weak forward Bisimulations, using the concept of a weak forward isomorphism instead of an isomorphism. We also give examples that explain the relationships between the considered types of Bisimulations.
-
Bisimulations for fuzzy automata
Fuzzy Sets and Systems, 2012Co-Authors: Miroslav Ćirić, Jelena Ignjatović, Nada Damljanović, Milan BašićAbstract:Bisimulations have been widely used in many areas of computer science to model equivalence between various systems, and to reduce the number of states of these systems, whereas uniform fuzzy relations have recently been introduced as a means to model the fuzzy equivalence between elements of two possible different sets. Here we use the conjunction of these two concepts as a powerful tool in the study of equivalence between fuzzy automata. We prove that a uniform fuzzy relation between fuzzy automata A and B is a forward Bisimulation if and only if its kernel and co-kernel are forward Bisimulation fuzzy equivalence relations on A and B and there is a special isomorphism between factor fuzzy automata with respect to these fuzzy equivalence relations. As a consequence we get that fuzzy automata A and B are UFB-equivalent, i.e., there is a uniform forward Bisimulation between them, if and only if there is a special isomorphism between the factor fuzzy automata of A and B with respect to their greatest forward Bisimulation fuzzy equivalence relations. This result reduces the problem of testing UFB-equivalence to the problem of testing isomorphism of fuzzy automata, which is closely related to the well-known graph isomorphism problem. We prove some similar results for backward-forward Bisimulations, and we point to fundamental differences. Because of the duality with the studied concepts, backward and forward-backward Bisimulations are not considered separately. Finally, we give a comprehensive overview of various concepts on deterministic, nondeterministic, fuzzy, and weighted automata, which are related to Bisimulations.
-
Bisimulations for fuzzy automata
arXiv: Formal Languages and Automata Theory, 2011Co-Authors: Miroslav Ćirić, Jelena Ignjatović, Nada Damljanović, Milan BašićAbstract:Bisimulations have been widely used in many areas of computer science to model equivalence between various systems, and to reduce the number of states of these systems, whereas uniform fuzzy relations have recently been introduced as a means to model the fuzzy equivalence between elements of two possible different sets. Here we use the conjunction of these two concepts as a powerful tool in the study of equivalence between fuzzy automata. We prove that a uniform fuzzy relation between fuzzy automata $\cal A$ and $\cal B$ is a forward Bisimulation if and only if its kernel and co-kernel are forward Bisimulation fuzzy equivalences on $\cal A$ and $\cal B$ and there is a special isomorphism between factor fuzzy automata with respect to these fuzzy equivalences. As a consequence we get that fuzzy automata $\cal A$ and $\cal B$ are UFB-equivalent, i.e., there is a uniform forward Bisimulation between them, if and only if there is a special isomorphism between the factor fuzzy automata of $\cal A$ and $\cal B$ with respect to their greatest forward Bisimulation fuzzy equivalences. This result reduces the problem of testing UFB-equivalence to the problem of testing isomorphism of fuzzy automata, which is closely related to the well-known graph isomorphism problem. We prove some similar results for backward-forward Bisimulations, and we point to fundamental differences. Because of the duality with the studied concepts, backward and forward-backward Bisimulations are not considered separately. Finally, we give a comprehensive overview of various concepts on deterministic, nondeterministic, fuzzy, and weighted automata, which are related to Bisimulations.
Jonathan May - One of the best experts on this subject based on the ideXlab platform.
-
Backward and forward Bisimulation minimization of tree automata
Theoretical Computer Science, 2009Co-Authors: Johanna Hogberg, Andreas Maletti, Jonathan MayAbstract:AbstractWe improve on an existing [P.A. Abdulla, J. Högberg, L. Kaati, Bisimulation minimization of tree automata, International Journal of Foundations of Computer Science 18(4) (2007) 699–713] Bisimulation minimization algorithm for finite-state tree automata by introducing backward and forward Bisimulation and developing minimization algorithms for them. Minimization via forward Bisimulation is also effective on deterministic tree automata, faster than the previous algorithm, and yields the minimal equivalent deterministic tree automaton. Minimization via backward Bisimulation generalizes the previous algorithm and can yield smaller automata but is just as fast. We demonstrate implementations of these algorithms on a typical task in natural language processing
-
backward and forward Bisimulation minimisation of tree automata
International Conference on Implementation and application of automata, 2007Co-Authors: Johanna Hogberg, Andreas Maletti, Jonathan MayAbstract:We improve an existing Bisimulation minimisation algorithm for tree automata by introducing backward and forward Bisimulations and developing minimisation algorithms for them. Minimisation via forward Bisimulation is also effective for deterministic automata and faster than the previous algorithm. Minimisation via backward Bisimulation generalises the previous algorithm and is thus more effective but just as fast. We demonstrate implementations of these algorithms on a typical task in natural language processing.
