Bounded model checking of ETL cooperating with finite and looping automata connectives

DOI10.1155/2013/462532MaRDI QIDQ364388zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Wanwei Liu, Tun Li, Xiaoguang Mao, Ji Wang, Rui Wang

Publication date 9 September 2013

Published in Journal of Applied Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1155/2013/462532

Mathematics Subject Classification ID

Temporal logic (03B44) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

Summary: As a complementary technique of the BDD-based approach, bounded model checking (BMC) has been successfully applied to LTL symbolic model checking. However, the expressiveness of LTL is rather limited, and some important properties cannot be captured by such logic. In this paper, we present a semantic BMC encoding approach to deal with the mixture of \(\text{ETL}_f\) and \(\text{ETL}_l\). Since such kind of temporal logic involves both finite and looping automata as connectives, all regular properties can be succinctly specified with it. The presented algorithm is integrated into the model checker ENuSMV, and the approach is evaluated via conducting a series of imperial experiments.

Recommendations

• Bounded model checking for the existential fragment of \(\mathrm{TCTL}_{-G}\) and diagonal timed automata
• Bounded model checking for all regular properties
• scientific article; zbMATH DE number 2086516
• Bounded model checking of infinite state systems
• scientific article; zbMATH DE number 1799521

Cites work

• Automated Technology for Verification and Analysis
• Bounded model checking for all regular properties
• Büchi complementation made tight
• Computer Aided Verification
• Formal Methods in Computer-Aided Design
• Graph-Based Algorithms for Boolean Function Manipulation
• scientific article; zbMATH DE number 3919813 (Why is no real title available?)
• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 2080056 (Why is no real title available?)
• scientific article; zbMATH DE number 1796144 (Why is no real title available?)
• Linear Encodings of Bounded LTL Model Checking
• Lower Bounds for Complementation of omega-Automata Via the Full Automata Technique
• Reasoning about infinite computations
• Regular Linear Temporal Logic
• Temporal logic can be more expressive
• The complementation problem for Büchi automata with applications to temporal logic
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Weak alternating automata are not that weak

Cited in

(2)

• ENuSMV
• Bounded model checking for all regular properties

Describes a project that uses

Uses Software

• NuSMV

This page was built for publication: Bounded model checking of ETL cooperating with finite and looping automata connectives

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