On the complexity of verifying concurrent transition systems

DOI10.1007/3-540-63141-0_18MaRDI QIDQ6044122zbMATH OpenOpenAlexFDO

Authors David Harel, Orna Kupferman, Moshe Y. Vardi

Publication date 17 May 2023

Published in CONCUR '97: Concurrency Theory (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-63141-0_18

Mathematics Subject Classification ID

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

Recommendations

• On the complexity of verifying concurrent transition systems
• The fixed-parameter tractability of model checking concurrent systems
• Verification of concurrent programs: The automata-theoretic framework
• Verification of concurrent systems with VerCors
• Concurrency based transition refinement for the verification of distributed algorithms
• On the complexity of verification of time-sensitive distributed systems
• scientific article; zbMATH DE number 1897216
• scientific article; zbMATH DE number 967185
• Specification and verification of concurrent systems by causality and realizability
• Compositional verification of concurrent systems by combining bisimulations

Cites work

• A calculus of communicating systems
• Alternation
• Deciding bisimilarity is P-complete
• Equivalences for fair Kripke structures
• scientific article; zbMATH DE number 3735115 (Why is no real title available?)
• scientific article; zbMATH DE number 17792 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• On the power of bounded concurrency I
• On the power of bounded concurrency II
• Protocol Verification via Projections
• Reasoning about infinite computations
• Statecharts: a visual formalism for complex systems
• The complementation problem for Büchi automata with applications to temporal logic
• The existence of refinement mappings

Cited in

(15)

• Checking simple properties of transition systems defined by Thue specifications
• Alternation and bounded concurrency are reverse equivalent.
• On the complexity of verifying concurrent transition systems
• Is your model checker on time? On the complexity of model checking for timed modal logics
• Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
• Formalization and correctness of a concurrent linear hash structure algorithm using nested transactions and I/O automata
• Proceedings of the workshop on graph transformation for concurrency and verification (GT-VC 2006), Bonn, Germany, August 31, 2006
• The Complexity of Reliable Concurrency Control
• scientific article; zbMATH DE number 1332671 (Why is no real title available?)
• On the Complexity of Bounded Context Switching.
• scientific article; zbMATH DE number 7167584 (Why is no real title available?)
• On the Complexity of Verifying Regular Properties on Flat Counter Systems,
• Tools and Algorithms for the Construction and Analysis of Systems
• Hardness of preorder checking for basic formalisms
• A consistency analysis of a class of concurrent transient implicit/explicit algorithms

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6044122)