A classification of symbolic transition systems

DOI10.1145/1042038.1042039zbMath1367.68193OpenAlexW1977116278MaRDI QIDQ5277714

Rupak Majumdar, Jean-François Raskin, Thomas A. Henzinger

Publication date: 12 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1042038.1042039

zbMATH Keywords

hybrid automatamodel checkingtemporal logicssymbolic algorithmsinfinite-state model checkingstate equivalences

Mathematics Subject Classification ID

Formal languages and automata (68Q45) 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 (18)

Symbolic model checking for probabilistic timed automata ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ A deductive approach towards reasoning about algebraic transition systems ⋮ Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications ⋮ Fine-grained complexity lower bounds for problems in computer aided verification ⋮ A Simpler Alternative: Minimizing Transition Systems Modulo Alternating Simulation Equivalence ⋮ Weighted o-minimal hybrid systems ⋮ Generalizing the Paige-Tarjan algorithm by abstract interpretation ⋮ Multiply-Recursive Upper Bounds with Higman’s Lemma ⋮ Computable fixpoints in well-structured symbolic model checking ⋮ Verification of qualitative \(\mathbb Z\) constraints ⋮ A classification of the expressive power of well-structured transition systems ⋮ LTL over integer periodicity constraints ⋮ Model Refinement Using Bisimulation Quotients ⋮ A Language-Based Comparison of Extensions of Petri Nets with and without Whole-Place Operations ⋮ Probabilistic and Topological Semantics for Timed Automata ⋮ Symbolic Execution Based Model Checking of Open Systems with Unbounded Variables ⋮ How to Tackle Integer Weighted Automata Positivity

This page was built for publication: A classification of symbolic transition systems