Characterizing finite Kripke structures in propositional temporal logic
From MaRDI portal
Publication:1123183
DOI10.1016/0304-3975(88)90098-9zbMath0677.03011OpenAlexW1990183105MaRDI QIDQ1123183
Orna Grumberg, M. C. Browne, Edmund M. Clarke
Publication date: 1988
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(88)90098-9
Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Abstract data types; algebraic specification (68Q65) Nonclassical models (Boolean-valued, sheaf, etc.) (03C90)
Related Items (68)
Model checking for action-based logics ⋮ Characteristic formulae for fixed-point semantics: a general framework ⋮ An O ( m log n ) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation ⋮ Taming the complexity of biochemical models through bisimulation and collapsing: theory and practice ⋮ Applicability of fair simulation ⋮ LTL receding horizon control for finite deterministic systems ⋮ Partial-Order Reduction ⋮ Abstraction and Abstraction Refinement ⋮ Behavioural characterizations of partial order logics ⋮ Algebraic simulations ⋮ Geometric Model Checking of Continuous Space ⋮ Interleaving isotactics -- an equivalence notion on behaviour abstractions ⋮ Computing Stuttering Simulations ⋮ Feature interaction detection by pairwise analysis of LTL properties -- A case study ⋮ Comparative branching-time semantics for Markov chains ⋮ Invariance under stuttering in a temporal logic of actions ⋮ Reasoning about equilibria in game-like concurrent systems ⋮ Parity game reductions ⋮ Synthesis of large dynamic concurrent programs from dynamic specifications ⋮ A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures ⋮ An invariant-based approach to the verification of asynchronous parameterized networks ⋮ To be fair, use bundles ⋮ On the expressivity and complexity of quantitative branching-time temporal logics ⋮ Branching vs. Linear Time: Semantical Perspective ⋮ State equivalences for rectangular hybrid automata ⋮ Back-and-forth in space: on logics and bisimilarity in closure spaces ⋮ A Markovian model for the spread of the SARS-CoV-2 virus ⋮ The Birth of Model Checking ⋮ On the composition of time Petri nets ⋮ Bisimilar linear systems. ⋮ Reasoning about networks with many identical finite state processes ⋮ Generalizing the Paige-Tarjan algorithm by abstract interpretation ⋮ Models of nondeterministic regular expressions ⋮ On Reasoning About Rings ⋮ Control machines: A new model of parallelism for compositional specifications and their effective compilation ⋮ Equivalences for fair Kripke structures ⋮ Compositionality and bisimulation: A negative result ⋮ Characteristic Formulae for Timed Automata ⋮ Deciding orthogonal bisimulation ⋮ A hierarchy of temporal logics with past ⋮ Equational abstractions ⋮ An automatic abstraction technique for verifying featured, parameterised systems ⋮ Dynamical systems in categories ⋮ Modular abstractions for verifying real-time distributed systems ⋮ Universal axioms for bisimulations ⋮ Automatic verification of distributed systems: the process algebra approach. ⋮ Unnamed Item ⋮ Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes ⋮ Well-structured transition systems everywhere! ⋮ Smaller Abstractions for ∀CTL* without Next ⋮ Unnamed Item ⋮ A general approach to comparing infinite-state systems with their finite-state specifications ⋮ Reconciling statechart semantics ⋮ Folk Theorems on the Correspondence between State-Based and Event-Based Systems ⋮ Symbolic Branching Bisimulation-Checking of Dense-Time Systems in an Environment ⋮ Bisimilarity Minimization in O(m logn) Time ⋮ Formal Verification for Components and Connectors ⋮ Group-by-Group Probabilistic Bisimilarities and Their Logical Characterizations ⋮ Probabilistic weak simulation is decidable in polynomial time ⋮ Game-theoretic simulation checking tool ⋮ Towards a unified view of bisimulation: A comparative study ⋮ An efficient simulation algorithm based on abstract interpretation ⋮ Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models ⋮ A partial order approach to branching time logic model checking. ⋮ Module checking ⋮ The complexity of propositional linear temporal logics in simple cases ⋮ Parameterised verification for multi-agent systems ⋮ Combining symmetry reduction and under-approximation for symbolic model checking
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The temporal logic of branching time
- Hierarchical verification of asynchronous circuits using temporal logic
- A linear algorithm to solve fixed-point equations on transition systems
- A calculus of communicating systems
- Synthesis of Communicating Processes from Temporal Logic Specifications
- The power of the future perfect in program logics
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Deciding full branching time logic
- Automatic Verification of Sequential Circuits Using Temporal Logic
- The complexity of propositional linear temporal logics
This page was built for publication: Characterizing finite Kripke structures in propositional temporal logic
