Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages

DOI10.1007/978-3-540-78800-3_2MaRDI QIDQ5458316zbMATHOpenAlexFDO

Authors Azadeh Farzan, Yu-Fang Chen, Yih-Kuen Tsay, Bow-Yaw Wang, Edmund Clarke

Publication date 11 April 2008

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78800-3_2

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Computational learning theory (68Q32) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• On the learnability of infinitary regular sets
• Learning Meets Verification
• Tools and Algorithms for the Construction and Analysis of Systems
• AUTOMATED COMPOSITIONAL REASONING OF INTUITIONISTICALLY CLOSED REGULAR PROPERTIES
• Learning Algorithms and Formal Verification (Invited Tutorial)

Cited in

(32)

• Tools and Algorithms for the Construction and Analysis of Systems
• Inferring switched nonlinear dynamical systems
• Learning infinite-word automata with loop-index queries
• Learning Algorithms and Formal Verification (Invited Tutorial)
• Learning Minimal Separating DFA’s for Compositional Verification
• Compositional probabilistic verification through multi-objective model checking
• Families of DFAs as acceptors of \(\omega\)-regular languages
• Assume-guarantee reasoning with local specifications
• Regular \(\omega\)-languages with an informative right congruence
• Computer Aided Verification
• Polynomial identification of \(\omega \)-automata
• Query learning of derived \(\omega\)-tree languages in polynomial time
• Relational Methods in Computer Science
• AUTOMATED COMPOSITIONAL REASONING OF INTUITIONISTICALLY CLOSED REGULAR PROPERTIES
• How hard is finding shortest counter-example lassos in model checking?
• Inferring regular languages and \(\omega\)-languages
• Concurrent Kleene algebra with observations: from hypotheses to completeness
• scientific article; zbMATH DE number 7447748 (Why is no real title available?)
• Automated Compositional Reasoning of Intuitionistically Closed Regular Properties
• A novel learning algorithm for Büchi automata based on family of DFAs and classification trees
• Learning one-clock timed automata
• Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys
• Compositional verification and 3-valued abstractions join forces
• Learning regular omega languages
• A class of automata for the verification of infinite, resource-allocating behaviours
• A framework for compositional verification of multi-valued systems via abstraction-refinement
• Deciding monadic second order logic over \(\omega \)-words by specialized finite automata
• Testing language containment for \(\omega\)-automata using BDDs
• A novel learning algorithm for Büchi automata based on family of DFAs and classification trees
• Mediating for reduction (on minimizing alternating Büchi automata)
• Compositional reasoning
• Constructing deterministic parity automata from positive and negative examples

Describes a project that uses

Uses Software

• LTL2BA

This page was built for publication: Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages

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