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

DOI10.1007/978-3-540-78800-3_2MaRDI QIDQ5458316zbMATH OpenOpenAlexFDO

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)

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

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)