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

DOI10.1155/2013/462532zbMath1311.68090OpenAlexW2053008981WikidataQ59006099 ScholiaQ59006099MaRDI QIDQ364388

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

Publication date: 9 September 2013

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

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

Mathematics Subject Classification ID

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

Related Items (1)

ENuSMV

Uses Software

• NuSMV

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The complementation problem for Büchi automata with applications to temporal logic
• Reasoning about infinite computations
• Temporal logic can be more expressive
• Lower Bounds for Complementation of omega-Automata Via the Full Automata Technique
• Regular Linear Temporal Logic
• Weak alternating automata are not that weak
• Graph-Based Algorithms for Boolean Function Manipulation
• Linear Encodings of Bounded LTL Model Checking
• Büchi Complementation Made Tight
• Automated Technology for Verification and Analysis
• Formal Methods in Computer-Aided Design
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation

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