A minimized automaton representation of reachable states

DOI10.1007/s100090050034zbMath1065.68579OpenAlexW2044309072MaRDI QIDQ1856175

Gerard J. Holzmann, Anuj Puri

Publication date: 1999

Published in: International Journal on Software Tools for Technology Transfer. STTT (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s100090050034

zbMATH Keywords

verificationdata compressionmodel checkingfinite automataOBDDsSPINsharing trees

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Coding and information theory (compaction, compression, models of communication, encoding schemes, etc.) (aspects in computer science) (68P30)

Related Items

An efficient algorithm for computing bisimulation equivalence, An invariant-based approach to the verification of asynchronous parameterized networks, Flash memory efficient LTL model checking, Minimization of Visibly Pushdown Automata Using Partial Max-SAT, More efficient on-the-fly LTL verification with Tarjan's algorithm, On automation in the verification of software barriers: experience report

Uses Software

• SPIN