Model-checking infinite state-space systems with fine-grained abstractions using SPIN

DOI10.1007/3-540-45139-0_3MaRDI QIDQ4531751zbMATH OpenFDO

Authors Marsha Chechik, Benet Devereux, Arie Gurfinkel

Publication date 23 May 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2057/20570016

Mathematics Subject Classification ID

Many-valued logic (03B50) Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Infinite state model checking by abstract interpretation and program specialisation
• Computer Science Logic
• Model checking guided abstraction and analysis
• On model checking infinite-state systems
• An automata-theoretic approach to infinite-state systems

Cited in

(17)

• Latticed-LTL synthesis in the presence of noisy inputs
• Weighted automata
• Computation tree logic model checking based on multi-valued possibility measures
• Beyond vacuity: towards the strongest passing formula
• Model checking of linear-time properties in multi-valued systems
• Inherent vacuity in lattice automata
• Latticed Simulation Relations and Games
• Don't know for multi-valued systems
• Multi-valued model checking games
• Linear temporal logic symbolic model checking
• Model Checking Quantitative Linear Time Logic
• Lattice Automata
• Formal verification of three-valued digital waveforms
• Minimizing deterministic lattice automata
• An abstraction-refinement framework for verifying strategic properties in multi-agent systems with imperfect information
• Robustness of temporal logic specifications for continuous-time signals
• Weighted automata and multi-valued logics over arbitrary bounded lattices

This page was built for publication: Model-checking infinite state-space systems with fine-grained abstractions using SPIN

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4531751)