Bounded rational search for on-the-fly model checking of LTL properties

DOI10.1007/978-3-642-11623-0_17zbMATH Open1274.68175OpenAlexW1512485549MaRDI QIDQ3400928FDOQ3400928

Authors: Razieh Behjati, Marjan Sirjani, M. Nili Ahmadabadi 

Publication date: 28 January 2010

Published in: Fundamentals of Software Engineering (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-11623-0_17

Recommendations

• Component-wise incremental LTL model checking
• On-the-fly probabilistic model checking
• Tools and Algorithms for the Construction and Analysis of Systems
• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
• Memory-efficient tactics for randomized LTL model checking

zbMATH Keywords

reinforcement learningapproximate probabilistic model checkingconcurrent systems verification

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)

Cited In (2)

• Automated Technology for Verification and Analysis
• Checking Liveness Properties of Concurrent Systems by Reinforcement Learning

Uses Software

• APMC

This page was built for publication: Bounded rational search for on-the-fly model checking of LTL properties

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