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

Computational learning theory (68Q32) Formal languages and automata (68Q45) 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

(33)

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

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)