Characterizing finite Kripke structures in propositional temporal logic
From MaRDI portal
A (finite) Kripke structure is a triple \(M=<S,R,{\mathcal L}>\), where S is the (finite) set of states, \(R\subseteq S\times S\) is a (total) transition relation and \({\mathcal L}\) is a valuation from states to the set of subsets of atomic formulas of a given (propositional) temporal logic theory \({\mathcal T}\). The chosen logics are \(CTL^*\) [\textit{E. A. Emerson} and \textit{J. Y. Halpern}, J. Assoc. Comput. Mach. 33, 151-178 (1986; Zbl 0629.68020)] and CTL. CTL is a restricted subset of \(CTL^*\) that permits only branching time operators (linear time operator being disallowed) such that each path quantifier must be immediately followed by exactly one of the operators G (``always), F (``sometimes), X (``next time) or U (``until). It is shown that if two finite Kripke structures can be distinguished (via valid formulas) in \(CTL^*\), then they can also be distinguished in CTL. The formulas implied characterize the Kripke structures via a natural equivalence relation (similar to bisimulation), or via a ``stuttering relation (by eliminating the ``next time operator). A polynomial time algorithm for computing the equivalence relation via stuttering is also given.
Recommendations
- Augmenting branching temporal logics with existential quantification over atomic propositions
- scientific article; zbMATH DE number 4016870
- A quantitative characterization of weighted Kripke structures in temporal logic
- Computation tree logic with deadlock detection
- A quantitative characterization of weighted Kripke structures in temporal logic
- scientific article; zbMATH DE number 2084388
- Logics and decidability for labelled pre- and partially ordered Kripke structures
- scientific article; zbMATH DE number 177267
- Kripke incompleteness of first-order calculi with temporal modalities of CTL and near logics
- Temporal logic CTL \(+\) Prolog
Cites work
- A calculus of communicating systems
- A linear algorithm to solve fixed-point equations on transition systems
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Automatic Verification of Sequential Circuits Using Temporal Logic
- Deciding full branching time logic
- Hierarchical verification of asynchronous circuits using temporal logic
- scientific article; zbMATH DE number 3870578 (Why is no real title available?)
- scientific article; zbMATH DE number 3913664 (Why is no real title available?)
- scientific article; zbMATH DE number 3919813 (Why is no real title available?)
- scientific article; zbMATH DE number 3688686 (Why is no real title available?)
- Synthesis of Communicating Processes from Temporal Logic Specifications
- The complexity of propositional linear temporal logics
- The power of the future perfect in program logics
- The temporal logic of branching time
Cited in
(82)- Reconciling statechart semantics
- Probabilistic weak simulation is decidable in polynomial time
- An efficient simulation algorithm based on abstract interpretation
- Control machines: A new model of parallelism for compositional specifications and their effective compilation
- Compositionality and bisimulation: A negative result
- Model checking for action-based logics
- Logics and decidability for labelled pre- and partially ordered Kripke structures
- On the expressivity and complexity of quantitative branching-time temporal logics
- Bisimilar linear systems.
- Towards a unified view of bisimulation: A comparative study
- Interleaving isotactics -- an equivalence notion on behaviour abstractions
- Parity game reductions
- A partial order approach to branching time logic model checking.
- Module checking
- The complexity of propositional linear temporal logics in simple cases
- Taming the complexity of biochemical models through bisimulation and collapsing: theory and practice
- Applicability of fair simulation
- Models of nondeterministic regular expressions
- Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
- Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
- Comparative branching-time semantics for Markov chains
- To be fair, use bundles
- Deciding orthogonal bisimulation
- A general approach to comparing infinite-state systems with their finite-state specifications
- Parameterised verification for multi-agent systems
- LTL receding horizon control for finite deterministic systems
- Characteristic formulae for timed autoamta
- Group-by-group probabilistic bisimilarities and their logical characterizations
- Distributed branching bisimulation reduction of state spaces
- Characteristic formulae for fixed-point semantics: a general framework
- scientific article; zbMATH DE number 4016870 (Why is no real title available?)
- Folk Theorems on the Correspondence between State-Based and Event-Based Systems
- Partial-Order Reduction
- Abstraction and abstraction refinement
- Computing Stuttering Simulations
- Reasoning about equilibria in game-like concurrent systems
- Synthesis of large dynamic concurrent programs from dynamic specifications
- Branching vs. Linear Time: Semantical Perspective
- The Birth of Model Checking
- Symbolic Branching Bisimulation-Checking of Dense-Time Systems in an Environment
- Bisimilarity Minimization in O(m logn) Time
- Formal Verification for Components and Connectors
- scientific article; zbMATH DE number 177516 (Why is no real title available?)
- Equivalences for fair Kripke structures
- Behavioural characterizations of partial order logics
- Geometric Model Checking of Continuous Space
- scientific article; zbMATH DE number 7559464 (Why is no real title available?)
- Dynamical systems in categories
- Smaller Abstractions for ∀CTL* without Next
- An O(m n) algorithm for computing stuttering equivalence and branching bisimulation
- On Reasoning About Rings
- Well-structured transition systems everywhere!
- An invariant-based approach to the verification of asynchronous parameterized networks
- 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
- On the composition of time Petri nets
- An action based framework for verifying logical and behavioural properties of concurrent systems
- On bisimilarity for polyhedral models and \texttt{SLCS}
- Modal and temporal logics for processes
- A hierarchy of temporal logics with past
- Modular abstractions for verifying real-time distributed systems
- Universal axioms for bisimulations
- On bisimilarity for quasi-discrete closure spaces
- Modal logic characterizations of forward, reverse, and forward-reverse bisimilarities
- Computing minimal distinguishing Hennessy-Milner formulas is NP-hard, but variants are tractable
- Model and program repair via group actions and structure unwinding
- Compositional reasoning in model checking
- SAT-based learning of computation tree logic
- The complexity of deciding characteristic formulae in van Glabbeek's branching-time spectrum
- Unified bisimulation applied to incremental abstraction of Petri nets
- Game-theoretic simulation checking tool
- Combining symmetry reduction and under-approximation for symbolic model checking
- Algebraic simulations
- Feature interaction detection by pairwise analysis of LTL properties -- A case study
- Invariance under stuttering in a temporal logic of actions
- A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures
- Reasoning about networks with many identical finite state processes
- Generalizing the Paige-Tarjan algorithm by abstract interpretation
- Equational abstractions
- An automatic abstraction technique for verifying featured, parameterised systems
- Automatic verification of distributed systems: the process algebra approach.
This page was built for publication: Characterizing finite Kripke structures in propositional temporal logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1123183)
