Characterizing finite Kripke structures in propositional temporal logic
From MaRDI portal
Recommendations
- Augmenting branching temporal logics with existential quantification over atomic propositions
- Publication:3028984
- 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
- 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?)
- A calculus of communicating systems
- A linear algorithm to solve fixed-point equations on transition systems
- Automatic Verification of Sequential Circuits Using Temporal Logic
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Deciding full branching time logic
- Hierarchical verification of asynchronous circuits using temporal logic
- 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
(74)- Bisimilarity Minimization in O(m logn) Time
- An \(\mathcal O(m\log n)\) algorithm for computing stuttering equivalence and branching bisimulation
- A Markovian model for the spread of the SARS-CoV-2 virus
- Parameterised verification for multi-agent systems
- Geometric Model Checking of Continuous Space
- Formal Verification for Components and Connectors
- Applicability of fair simulation
- Modular abstractions for verifying real-time distributed systems
- Automatic verification of distributed systems: the process algebra approach.
- The Birth of Model Checking
- Taming the complexity of biochemical models through bisimulation and collapsing: theory and practice
- Modal and temporal logics for processes
- Partial-Order Reduction
- Model checking for action-based logics
- Computing Stuttering Simulations
- Reasoning about networks with many identical finite state processes
- Folk Theorems on the Correspondence between State-Based and Event-Based Systems
- State equivalences for rectangular hybrid automata
- Characteristic formulae for fixed-point semantics: a general framework
- Module checking
- Feature interaction detection by pairwise analysis of LTL properties -- A case study
- Probabilistic weak simulation is decidable in polynomial time
- Invariance under stuttering in a temporal logic of actions
- Group-by-group probabilistic bisimilarities and their logical characterizations
- Bisimilar linear systems.
- Logics and decidability for labelled pre- and partially ordered Kripke structures
- Back-and-forth in space: on logics and bisimilarity in closure spaces
- A partial order approach to branching time logic model checking.
- To be fair, use bundles
- Generalizing the Paige-Tarjan algorithm by abstract interpretation
- A hierarchy of temporal logics with past
- Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
- Interleaving isotactics -- an equivalence notion on behaviour abstractions
- On the composition of time Petri nets
- The complexity of propositional linear temporal logics in simple cases
- scientific article; zbMATH DE number 177516 (Why is no real title available?)
- Deciding orthogonal bisimulation
- Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
- Branching vs. Linear Time: Semantical Perspective
- A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures
- Parity game reductions
- An invariant-based approach to the verification of asynchronous parameterized networks
- Combining symmetry reduction and under-approximation for symbolic model checking
- Well-structured transition systems everywhere!
- Symbolic Branching Bisimulation-Checking of Dense-Time Systems in an Environment
- Abstraction and abstraction refinement
- An efficient simulation algorithm based on abstract interpretation
- scientific article; zbMATH DE number 4016870 (Why is no real title available?)
- Algebraic simulations
- Towards a unified view of bisimulation: A comparative study
- Game-theoretic simulation checking tool
- Control machines: A new model of parallelism for compositional specifications and their effective compilation
- Reasoning about equilibria in game-like concurrent systems
- Characteristic formulae for timed autoamta
- Universal axioms for bisimulations
- Equational abstractions
- Reconciling statechart semantics
- Compositionality and bisimulation: A negative result
- Synthesis of large dynamic concurrent programs from dynamic specifications
- An automatic abstraction technique for verifying featured, parameterised systems
- Models of nondeterministic regular expressions
- On Reasoning About Rings
- Smaller Abstractions for ∀CTL* without Next
- Equivalences for fair Kripke structures
- Distributed branching bisimulation reduction of state spaces
- An action based framework for verifying logical and behavioural properties of concurrent systems
- Comparative branching-time semantics for Markov chains
- Behavioural characterizations of partial order logics
- A general approach to comparing infinite-state systems with their finite-state specifications
- LTL receding horizon control for finite deterministic systems
- On bisimilarity for polyhedral models and \texttt{SLCS}
- On the expressivity and complexity of quantitative branching-time temporal logics
- Dynamical systems in categories
- scientific article; zbMATH DE number 7559464 (Why is no real title available?)
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)
