Randomization helps in LTL model checking

DOI10.1007/3-540-44804-7_7MaRDI QIDQ4798037zbMATH OpenFDO

Authors Luboš Brim, M. Nečesal, I. Černá

Publication date 18 March 2003

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/2165/21650105.htm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Memory-efficient tactics for randomized LTL model checking
• Model checking concurrent programs with nondeterminism and randomization
• scientific article; zbMATH DE number 2090708
• Randomized partial checking revisited
• Lazy probabilistic model checking without determinisation
• Yet another look at LTL model checking
• On the expressiveness and complexity of randomization in finite state monitors
• Measuring progress of probabilistic LTL model checking
• Counterexamples in Probabilistic LTL Model Checking for Markov Chains

Cited in

(4)

• Memory-efficient tactics for randomized LTL model checking
• Randomized refinement checking of timed I/O automata
• Testing Spin's LTL formula conversion into Büchi automata with randomly generated input
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Randomization helps in LTL model checking

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