CCS expressions, finite state processes, and three problems of equivalence

DOI10.1016/0890-5401(90)90025-DzbMath0705.68063OpenAlexW2021473546MaRDI QIDQ918211

Paris C. Kanellakis, Scott A. Smolka

Publication date: 1990

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(90)90025-d

zbMATH Keywords

concurrency observational equivalence nondeterministic finite automata calculus of communicating systems algebra of communicating processes failure equivalence generalized partitioning strong observational equivalence

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Complexity of computation (including implicit computational complexity) (03D15)

Related Items

An O ( m log n ) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation, Time abstracted bisimulation: Implicit specifications and decidability, Unnamed Item, On divergence-sensitive weak probabilistic bisimilarity, An automated quantitative information flow analysis for concurrent programs, A Simpler Alternative: Minimizing Transition Systems Modulo Alternating Simulation Equivalence, Lowerbounds for Bisimulation by Partition Refinement, A Spatial Logic for Simplicial Models, Verifying abstractions of timed systems, Better automata through process algebra, Equivalence checking 40 years after: a review of bisimulation tools, Correct and efficient antichain algorithms for refinement checking, Distributed Markovian Bisimulation Reduction aimed at CSL Model Checking, Pushdown automata, multiset automata, and Petri nets, Branching time controllers for discrete event systems, An Incremental Bisimulation Algorithm, Symbolic computation of differential equivalences, Timing-Sensitive Information Flow Analysis for Synchronous Systems, Improved algorithms for computing the greatest right and left invariant Boolean matrices and their application, An exercise in the automatic verification of asynchronous designs, A note on the complexity of deciding bisimilarity of normed unary processes, Coalgebraic Symbolic Semantics, Deciding probabilistic automata weak bisimulation: theory and practice, Testing equivalence as a bisimulation equivalence, An efficient algorithm for computing bisimulation equivalence, An improvement of algorithms for solving interface equations, Minimal transition systems for history-preserving bisimulation, Causality, Behavioural Equivalences, and the Security of Cyberphysical Systems, A space-efficient simulation algorithm on probabilistic automata, Process Algebra and Model Checking, An efficient algorithm to determine probabilistic bisimulation, Dynamics Security Policies and Process Opacity for Timed Process Algebras, Priority and abstraction in process algebra, Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence, Unnamed Item, Compositional failure-based semantic models for basic LOTOS, Undecidable equivalences for basic parallel processes, Time-abstracted bisimulation: Implicit specifications and decidability, Deciding true concurrency equivalences on safe, finite nets, Nested semantics over finite trees are equationally hard, A Tutorial on Interactive Markov Chains, Computing Behavioral Relations for Probabilistic Concurrent Systems, SOS formats and meta-theory: 20 years after, Complexity of equivalence problems for concurrent systems of finite agents, Weak bisimulation for probabilistic timed automata, A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences, Translating between models of concurrency, On the decidability of process equivalences for the π-calculus, Translating FSP into LOTOS and networks of automata, On the decidability of process equivalences for the \(\pi\)-calculus, CCS with Replication in the Chomsky Hierarchy: The Expressive Power of Divergence, Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving, Interface automata for shared memory, A coalgebraic semantics for causality in Petri nets, On the greatest solutions to weakly linear systems of fuzzy relation inequalities and equations, Depletable channels: dynamics, behaviour, and efficiency in network design, Undecidability of domino games and hhp-bisimilarity., A coalgebraic perspective on linear weighted automata, Bisimulations for fuzzy automata, Nondeterministic automata: equivalence, bisimulations, and uniform relations, Weighted o-minimal hybrid systems, Modal transition systems with weight intervals, Deadlock-freedom in component systems with architectural constraints, Selected Ideas Used for Decidability and Undecidability of Bisimilarity, Model-checking process equivalences, Deciding true concurrency equivalences on finite safe nets (preliminary report), A succinct canonical register automaton model, On the tradeoff between compositionality and exactness in weak bisimilarity for integrated-time Markovian process calculi, Constructive logical characterizations of bisimilarity for reactive probabilistic systems, Distribution and locality of concurrent systems, On deciding some equivalences for concurrent processes, Compositionality in state space verification methods, Deciding bisimulation and trace equivalences for systems with many identical processes, Polynomial time decision algorithms for probabilistic automata, From generic partition refinement to weighted tree automata minimization, Computing the Maximum Bisimulation with Spiking Neural P Systems, Hybrid automata with finite bisimulations, Isomorphism of Regular Trees and Words, Applying model-checking to solve queries on semistructured data, The parallel complexity of coarsest set partition problems, An aperiodic set of 11 Wang tiles, An O(m log n) algorithm for branching bisimilarity on labelled transition systems, Causal Semantics for BPP Nets with Silent Moves, EXPTIME-completeness of thorough refinement on modal transition systems, Deciding bisimilarity is P-complete, Computation of the greatest simulations and bisimulations between fuzzy automata, Set graphs. II. Complexity of set graph recognition and similar problems, Revisiting causality, coalgebraically, Metrics for weighted transition systems: axiomatization and complexity, On the computational complexity of bisimulation, redux, Unnamed Item, A parametric analysis of the state-explosion problem in model checking, Contract-based discovery of Web services modulo simple orchestrators, Fuzzy relation equations and reduction of fuzzy automata, The quest for minimal quotients for probabilistic and Markov automata, On the metric-based approximate minimization of Markov chains, An axiomatic semantics for \(\mathsf{ioco} \underline{\mathsf{s}}\) conformance relation, Reduction of fuzzy automata by means of fuzzy quasi-orders, Model Refinement Using Bisimulation Quotients, Computation of the greatest right and left invariant fuzzy quasi-orders and fuzzy equivalences, Checking equivalences between concurrent systems of finite agents (Extended abstract), (Bi)simulations up-to characterise process semantics, Hardness of equivalence checking for composed finite-state systems, Formal Verification for Components and Connectors, A process algebra with distributed priorities, Approximated Reachability on Hybrid Automata: Falsification meets Certification, Bisimilarity on basic parallel processes, Exact performance equivalence: An equivalence relation for stochastic automata, On the expressive power of recursion, replication and iteration in process calculi, A complexity analysis of bisimilarity for value-passing processes, Efficient Coalgebraic Partition Refinement, A partition refinement algorithm for the \(\pi\)-calculus, On deciding trace equivalences for processes, Priorities in process algebras, Uniform strategies, rational relations and jumping automata, Deciding bisimilarity of normed context-free processes is in \(\Sigma_ 2^ p\), Unwinding biological systems, Operational and abstract semantics of the query language G-Log, Proving finiteness of CCS processes by non-standard semantics

Cites Work