A partial order approach to branching time logic model checking.

DOI10.1006/INCO.1998.2778MaRDI QIDQ1854268zbMATH OpenOpenAlexFDO

Authors Rob Gerth, Ruurd Kuiper, Wojciech Penczek, Doron 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

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

Recommendations

• scientific article; zbMATH DE number 1059330
• scientific article; zbMATH DE number 1507206
• Publication:4507826
• scientific article; zbMATH DE number 1361136
• Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic

Cites work

• scientific article; zbMATH DE number 4157900 (Why is no real title available?)
• scientific article; zbMATH DE number 4030996 (Why is no real title available?)
• scientific article; zbMATH DE number 177254 (Why is no real title available?)
• scientific article; zbMATH DE number 177511 (Why is no real title available?)
• scientific article; zbMATH DE number 177845 (Why is no real title available?)
• A calculus of communicating systems
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Characterizing finite Kripke structures in propositional temporal logic

Cited in

(31)

• Equivalence checking 40 years after: a review of bisimulation tools
• Partial-order reduction in the weak modal mu-calculus
• The inconsistent labelling problem of stutter-preserving partial-order reduction
• Deciding global partial-order properties
• Modalities for model checking: Branching time logic strikes back
• A survey on temporal logics for specifying and verifying real-time systems
• Stubborn set reduction for timed reachability and safety games
• Compositional verification of concurrent systems by combining bisimulations
• Adding partial orders to linear temporal logic
• Partial-Order Reduction
• Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic
• scientific article; zbMATH DE number 177510 (Why is no real title available?)
• Translating Java for multiple model checkers: The Bandera back-end
• scientific article; zbMATH DE number 1507206 (Why is no real title available?)
• Partial order reduction for checking LTL formulae with the next-time operator
• Stubborn set reduction for two-player reachability games
• Taking Some Burden Off an Explicit CTL Model Checker
• Partial-order reduction for parity games with an application on parameterised Boolean equation systems
• Compositionality in state space verification methods
• Combining partial-order reductions with on-the-fly model-checking.
• Exponential automatic amortized resource analysis
• scientific article; zbMATH DE number 1515293 (Why is no real title available?)
• Partial model checking using networks of labelled transition systems and Boolean equation systems
• A comparison of confluence and ample sets in probabilistic and non-probabilistic branching time
• Question-guided stubborn set methods for state properties
• On stubborn sets in the verification of linear time temporal properties
• scientific article; zbMATH DE number 7407780 (Why is no real title available?)
• Model-checking games for fixpoint logics with partial order models
• Transparent partial order reduction
• Confluence for process verification
• Branching bisimulation games

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

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