Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
From MaRDI portal
Publication:5458316
DOI10.1007/978-3-540-78800-3_2zbMath1134.68406OpenAlexW2103976262MaRDI QIDQ5458316
Bow-Yaw Wang, Azadeh Farzan, Yu-Fang Chen, Yih-Kuen Tsay, Edmund M. 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
Computational learning theory (68Q32) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Learning infinite-word automata with loop-index queries, Learning One-Clock Timed Automata, Compositional Reasoning, Learning regular omega languages, Inferring regular languages and \(\omega\)-languages, Unnamed Item, Compositional probabilistic verification through multi-objective model checking, Concurrent Kleene algebra with observations: from hypotheses to completeness, Unnamed Item, A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees, Polynomial Identification of $$\omega $$-Automata, Compositional verification and 3-valued abstractions join forces, Automated Compositional Reasoning of Intuitionistically Closed Regular Properties, Regular \(\omega\)-languages with an informative right congruence, Efficient Unlinkable Sanitizable Signatures from Signatures with Re-randomizable Keys, Learning Minimal Separating DFA’s for Compositional Verification, Mediating for reduction (on minimizing alternating Büchi automata), A Class of Automata for the Verification of Infinite, Resource-Allocating Behaviours, Inferring switched nonlinear dynamical systems, Deciding Monadic Second Order Logic over $$\omega $$ ω -Words by Specialized Finite Automata, A novel learning algorithm for Büchi automata based on family of DFAs and classification trees, Unnamed Item, ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS, A framework for compositional verification of multi-valued systems via abstraction-refinement
Uses Software
