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

DOI10.1007/978-3-642-11623-0_17MaRDI QIDQ3400928zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(2)

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

Describes a project that uses

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)