A general approach to comparing infinite-state systems with their finite-state specifications
From MaRDI portal
Publication:2503044
DOI10.1016/j.tcs.2006.01.021zbMath1097.68075OpenAlexW2104378808MaRDI QIDQ2503044
Philippe Schnoebelen, Antonín Kučera
Publication date: 13 September 2006
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2006.01.021
Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items (5)
Characteristic formulae for fixed-point semantics: a general framework ⋮ A generic framework for checking semantic equivalences between pushdown automata and finite-state automata ⋮ Characteristic invariants in Hennessy-Milner logic ⋮ Computable fixpoints in well-structured symbolic model checking ⋮ Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Undecidability of bisimilarity for Petri nets and some related problems
- Characterizing finite Kripke structures in propositional temporal logic
- Characteristic formulae for processes with divergence
- A polynomial algorithm for deciding bisimilarity of normed context-free processes
- \(L(A)=L(B)\)? decidability results from complete formal systems
- On finite representations of infinite-state behaviours
- Impossible futures and determinism
- Verifying lossy channel systems has nonprimitive recursive complexity.
- Algorithmic analysis of programs with well quasi-ordered domains.
- Simulation preorder over simple process algebras
- Verifying programs with unreliable channels
- Decidability of bisimulation equivalence for process generating context-free languages
- On Communicating Finite-State Machines
- Three logics for branching bisimulation
- Branching time and abstraction in bisimulation semantics
- A polynomial-time algorithm for deciding bisimulation equivalence of normed Basic Parallel Processes
- A Logical Viewpoint on Process-algebraic Quotients
- Decidability of model checking with the temporal logic EF
- Well-structured transition systems everywhere!
- Deciding bisimulation-like equivalences with finite-state processes
- The regular viewpoint on PA-processes
This page was built for publication: A general approach to comparing infinite-state systems with their finite-state specifications
