On the complexity of verifying concurrent transition systems

DOI10.1006/inco.2001.2920zbMath1009.68082OpenAlexW1966825814MaRDI QIDQ1854510

David Harel, Moshe Y. Vardi, Orna Kupferman

Publication date: 14 January 2003

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

Full work available at URL: https://doi.org/10.1006/inco.2001.2920

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (11)

Under-approximation of reachability in multivalued asynchronous networks ⋮ The computational complexity of scenario-based agent verification and design ⋮ Complexity of reachability problems for finite discrete dynamical systems ⋮ Sufficient conditions for reachability in automata networks with priorities ⋮ Reachability problems for sequential dynamical systems with threshold functions. ⋮ Predecessor existence problems for finite discrete dynamical systems ⋮ Modeling and analyzing social network dynamics using stochastic discrete graphical dynamical systems ⋮ PSPACE-completeness of modular supervisory control problems ⋮ A parametric analysis of the state-explosion problem in model checking ⋮ A Parametrized Analysis of Algorithms on Hierarchical Graphs ⋮ A Rice-style theorem for parallel automata

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The existence of refinement mappings
• The complementation problem for Büchi automata with applications to temporal logic
• Statecharts: a visual formalism for complex systems
• A calculus of communicating systems
• Deciding bisimilarity is P-complete
• Reasoning about infinite computations
• Complexity of equivalence problems for concurrent systems of finite agents
• Protocol Verification via Projections
• Alternation
• On the power of bounded concurrency I
• On the power of bounded concurrency II
• An automata-theoretic approach to branching-time model checking

This page was built for publication: On the complexity of verifying concurrent transition systems