Verification on infinite structures. (Q2760246)

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].