On the complexity of verifying concurrent transition systems
From MaRDI portal
Publication:1854510
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
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
