Verification on infinite structures.
The paper forms a chapter of the Handbook of Process Algebra and surveys system verification through infinite state (transition) systems. Equivalence testing of infinite-state models of parallel systems can be used for checking the semantics against an existing specification and model checking determines their properties within some logical system. This paper studies these questions for discrete systems while infinite-state structures based on hybrid or timed systems are neglected. The work uses sequentially labelled rewrite transition systems for studying Basic Parallel Processes (BPP), [Basic] Process Algebra ([B]PA), Multiset Automata (MSA), Pushdown Automata (PDA), as well as Finite State Automata (FSA) and Petri Nets (PN).NEWLINENEWLINE Results for these classes of processes are obtained for bisimulation equivalence and for weak bisimulation equivalence. Model checking was considered with respect to variants of branching time logics like Hennessay-Milner Logic (HML) and its slight extensions EF, EG and UB, and with respect to Computation Tree Logic (CTL) and Presburger Computation Tree Logic (PCTL). From linear time logics were considered Constrained Linear Temporal Logic (CLTL) enhancing Linear Time Logic (LTL) and variants thereof. On 79 pages, this work gives a complete, up to date and detailed list of results as they were known at that time.NEWLINENEWLINEFor the entire collection see [Zbl 0971.00006].
- Automated Technology for Verification and Analysis
- Automatic verification methods for finite state systems. International workshop, Grenoble, France, June 12-14, 1989. Proceedings
- scientific article; zbMATH DE number 52748
- Computer Science Logic
- Equivalence-checking with infinite-state systems: techniques and results
- Reachability is decidable for weakly extended process rewrite systems
- Types and trace effects for object orientation
- The complexity of bisimilarity-checking for one-counter processes.
- Weak bisimilarity and regularity of context-free processes is EXPTIME-hard
- A brief history of process algebra
- Simulation preorder over simple process algebras
- Complexity of deciding bisimilarity between normed BPA and normed BPP
- Bisimilarity on basic parallel processes
- Characteristic invariants in Hennessy-Milner logic
- Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems
- Bounded model checking of infinite state systems
- A generic framework for checking semantic equivalences between pushdown automata and finite-state automata
- Deciding probabilistic bisimilarity over infinite-state probabilistic systems
- A general approach to comparing infinite-state systems with their finite-state specifications
- Decidability of performance equivalence for basic parallel processes
- Model checking for process rewrite systems and a class of action-based regular properties
- Decidable first-order transition logics for PA-processes
- Finite approximations for model checking non-finite-state processes
- Bounded situation calculus action theories
- Narrowing and rewriting logic: from foundations to applications
- Progression and verification of situation calculus agents with bounded beliefs
- Partially-Commutative Context-Free Processes
- CCS with Replication in the Chomsky Hierarchy: The Expressive Power of Divergence
- On Recursion, Replication and Scope Mechanisms in Process Calculi
- Selected Ideas Used for Decidability and Undecidability of Bisimilarity
- Normed BPA vs. Normed BPP Revisited
- Reducing behavioural to structural properties of programs with procedures
- Game characterization of probabilistic bisimilarity, and applications to pushdown automata
- An automata-theoretic approach to the reachability analysis of RPPS systems
- Turing machines, transition systems, and interaction
- Undecidability of performance equivalence of Petri nets
- Normed processes, unique decomposition, and complexity of bisimulation equivalences
- On Decidability of LTL+Past Model Checking for Process Rewrite Systems
- Partially-commutative context-free processes: expressibility and tractability
- Automated Technology for Verification and Analysis
- Sequencing and intermediate acceptance: Axiomatisation and decidability of bisimilarity
- Refining the process rewrite systems hierarchy via ground tree rewrite systems
- Refining the process rewrite systems hierarchy via ground tree rewrite systems
- Simulation relations and applications in formal methods
- Reasoning about sequences of memory states
- Turing machines, transition systems, and interaction
- On the computational complexity of bisimulation, redux
- Model independent approach to probabilistic models
- Complete symbolic reachability analysis using back-and-forth narrowing
- Decidability issues for extended ping-pong protocols
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Theory of interaction
- Compositional verification of sequential programs with procedures
- Bouziane's transformation of the Petri net reachability problem and incorrectness of the related algorithm
- On the complexity of checking semantic equivalences between pushdown processes and finite-state processes
This page was built for publication: Verification on infinite structures.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2760246)
