Bounded model construction for monadic second-order logics

DOI10.1007/10722167_11MaRDI QIDQ2754076zbMATH OpenFDO

Authors Abdelwaheb Ayari, David Basin

Publication date 11 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/10722167_11

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• MONA implementation secrets
• Time-Bounded Verification
• MONA IMPLEMENTATION SECRETS
• Bounded model checking for all regular properties
• Monadic second order finite satisfiability and unbounded tree-width

Cited in

(5)

• Counting on CTL^*: On the expressive power of monadic path logic
• Verified decision procedures for MSO on words based on derivatives of regular expressions
• On complementation of nondeterministic finite automata without full determinization
• Backjumping for quantified Boolean logic satisfiability
• Relativizations for the logic-automata connection

Describes a project that uses

Uses Software

• MONA
• SATO

This page was built for publication: Bounded model construction for monadic second-order logics

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