Narrow Results

In this paper we introduce and study Mealy multiset automata, presenting some useful properties of multisets and comparing various approaches. We present the notions of bisimulation, observability, and behavior for Mealy multiset automata. We give a characterization of the bisimulation relation between two Mealy multiset automata, and a result relating their general behavior and sequential behavior. We define cascade and direct product of Mealy multiset automata. Then we introduce Mealy membrane automata corresponding to elementary P systems.

We extend an algorithm by Paige and Tarjan that solves the coarsest stable refinement problem to the domain of trees. The algorithm is used to minimize nondeterministic tree automata (NTA) with respect to bisimulation. We show that our algorithm has an overall complexity of , where is the maximum rank of any symbol in the input alphabet, m is the total size of the transition table, and n is the number of states.

We consider the equivalence problem for labeled Markov chains (LMCs), where each state is labeled with an observation. Two LMCs are equivalent if every finite sequence of observations has the same probability of occurrence in the two LMCs. We show that equivalence can be decided in polynomial time, using a reduction to the equivalence problem for probabilistic automata, which is known to be solvable in polynomial time. We provide an alternative algorithm to solve the equivalence problem, which is based on a new definition of bisimulation for probabilistic automata. We also extend the technique to decide the equivalence of weighted probabilistic automata.

Then, we consider the equivalence problem for labeled Markov decision processes (LMDPs), which asks given two LMDPs whether for every scheduler (i.e. way of resolving the nondeterministic decisions) for each of the processes, there exists a scheduler for the other process such that the resulting LMCs are equivalent. The decidability of this problem remains open. We show that the schedulers can be restricted to be observation-based, but may require infinite memory.

We address the problem of reducing the size of (nondeterministic, bottom-up) tree automata (TA) using suitable, language-preserving equivalences on the states of the automata. In particular, we propose the so-called composed bisimulation equivalence as a new language preserving equivalence. A composed bisimulation equivalence is defined in terms of two different relations, namely the upward and downward bisimulation equivalence. We provide simple and efficient algorithms for computing these relations. The notion of composed bisimulation equivalence is motivated by an attempt to obtain an equivalence that can provide better reductions than what currently known bisimulation-based approaches can offer, but which is not significantly more difficult to compute (and hence stays below the computational requirements of simulation-based reductions). The experimental results we present in the paper show that our composed bisimulation equivalence meets such requirements, and hence provides users of TA with a finer way to resolve the trade-off between the available degree of reduction and its cost.

Simulations of weighted tree automata (wta) are considered. It is shown how such simulations can be decomposed into simpler functional and dual functional simulations also called forward and backward simulations. In addition, it is shown in several cases (fields, commutative rings, NOETHERIAN semirings, semiring of natural numbers) that all equivalent wta M and N can be joined by a finite chain of simulations. More precisely, in all mentioned cases there is a single wta that simulates both M and N. Those results immediately yield decidability of equivalence provided that the semiring is finitely (and effectively) presented.

The definition of bisimulation suggests a partition-refinement step, which we show to be suitable for a saturation-based implementation. We compare our fully symbolic saturation-based implementation with the fastest extant bisimulation algorithms over a set of benchmarks, and conclude that it appears to be the fastest algorithm capable of computing the largest bisimulation over very large quotient spaces.

The distributed structure of CCS processes can be made explicit by assigning different locations to their parallel components. These locations then become part of what is observed of a process. The assignment of locations may be done statically, or dynamically as the execution proceeds. The dynamic approach was developed first, in Refs. [4,5], as it appeared to be more convenient for defining notions of location equivalence and preorder. Extending previous work by L. Aceto¹ we study here the static approach, which is more natural from an intuitive point of view, and more manageable for verification purposes. We define static notions of location equivalence and preorder, and show that they coincide with the dynamic ones. To establish the equivalence of the two location semantics, we introduce an intermediate transition system called occurrence system, which incorporates both notions of locality. This system supports a definition of local history preserving bisimulation for CCS, which is a third formulation of location equivalence.

Graph pattern matching that aims to seek out answer graphs in a data graph matching a provided graph, plays a fundamental role as a part of graph search for graph databases. “Matching” indicates that the two graphs are correlated, such as bisimulation, isomorphism, simulation, etc. The strictness of bisimulation is between simulation and isomorphism. Seldom work has been done to search for bisimulation subgraphs. This research focuses on the problem. The symbol $\ast$ is introduced to fundamental modal logic language, thereby yielding $ML+\ast$ language; the symbols ${\square }^{\ast }$ is added for forming $ML+\ast$ formulas. Then conclusions about graph bisimulations are shown. Subsequently, a theorem with detailed proof is presented, stating that $ML+\ast$ formulas characterize finite directed graphs modulo bisimulation. According to the conclusions and theorem, algorithms for finding subgraphs are proposed. After dividing the query graph, the match graphs undergo the characterization using $ML+\ast$ formulas. In the data graphs, by model checking the formulas, the answer graphs exhibiting bisimilarity to the match graphs are able to be captured.

Cyber-physical Systems (CPS) are widely used in all areas of life. Ensuring the correctness of CPS remains an enduring challenge during its development and design phases. One approach to ascertain the correctness of CPS is behavior equivalence based on bisimulation. However, whether the implementation development process develops in the right direction has an important impact on obtaining the correct system implementation. Especially, the development process of complex CPS often yields a multitude of implementation versions, the correlation among these versions partly signifies the correctness of the development process. This paper formalizes the relationship between the implementation versions and establishes a formal description of the development process progressing in the correct direction, leveraging the concept of a “limit idea.” Initially, we introduce the concept of “limit bisimulation” for CPS systems to delineate implementations acquired during the CPS development process. Specific limit bisimulations are demonstrated to represent distinct scenarios within the development process. Subsequently, the convergence mechanism of implementations is modeled through bisimulation limits, encapsulating the CPS’s specification as the ultimate goal of obtained implementations during the development process. Finally, the congruence property of the bisimulation limit is proved, which accounts for the relation between specification and implementation versions can be decomposed into a refinement hierarchy. The limit theorem of bisimulation in CPS can help the designer and developer of CPS to comprehend the development course better.

We prove that the category of $F$-coalgebras admits exact sequences, under condition $F$ preserves pullbacks; the underlying category ${𝒞}$ is assumed to be cocomplete with epi-(regular mono) factorizations, finite products and exact sequences.

Spiking Neural P Systems (SNP systems in short) are Turing complete computing models inspired by biological spiking neurons. In this work we relate SNP Systems with delay and those without delay using SNP algebra, a type of process algebra specifically for SNP systems. Given an initial configuration where only the initial neuron(s) fires a spike, i.e. the first set of neuron(s) to fire, we focus on four SNP system modules performing four spike routings: sequential, join, split, and iteration. We show that there exist bisimulations between the respective four modules of SNP systems with delays and the four modules without delays. We then use these modules (both with and without delays) to create larger SNP systems such that bisimulations also exist between them.

In this paper, we show that the two biogeochemical processes, carbon and nitrogen cycles are weakly bisimilar or weakly equivalent. We model each process as labeled transition system (LTS), where transitions between Carbon and Nitrogen states are movements from different compartment of Earth. We showed that there exist a binary relation over the states of the two systems, such that one weakly simulates the other with respect to their changes in location.