A partial order approach to branching time logic model checking.

DOI10.1006/inco.1998.2778zbMath1045.68588OpenAlexW2062081943MaRDI QIDQ1854268

Rob Gerth, Ruurd Kuiper, Wojciech Penczek, Doron A. Peled

Publication date: 14 January 2003

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

Full work available at URL: https://research.tue.nl/nl/publications/a-partial-order-approach-to-branching-time-logic-model-checking(97bbfaef-a151-4087-a869-c3564e1ec4ad).html

zbMATH Keywords

assertional language

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

Related Items (20)

Stubborn set reduction for timed reachability and safety games ⋮ Partial-Order Reduction ⋮ Compositional verification of concurrent systems by combining bisimulations ⋮ Question-guided stubborn set methods for state properties ⋮ Unnamed Item ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ Equivalence checking 40 years after: a review of bisimulation tools ⋮ Taking Some Burden Off an Explicit CTL Model Checker ⋮ Exponential automatic amortized resource analysis ⋮ The inconsistent labelling problem of stutter-preserving partial-order reduction ⋮ A comparison of confluence and ample sets in probabilistic and non-probabilistic branching time ⋮ Compositionality in state space verification methods ⋮ Confluence for process verification ⋮ Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems ⋮ Model-checking games for fixpoint logics with partial order models ⋮ On stubborn sets in the verification of linear time temporal properties ⋮ Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic ⋮ Branching Bisimulation Games ⋮ Unnamed Item ⋮ Translating Java for multiple model checkers: The Bandera back-end

Cites Work

• Characterizing finite Kripke structures in propositional temporal logic
• A calculus of communicating systems
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A partial order approach to branching time logic model checking.