Automata-Theoretic Model Checking Revisited

DOI10.1007/978-3-540-69738-1_10zbMATH Open1132.68483OpenAlexW1698053229MaRDI QIDQ5452603FDOQ5452603

Moshe Y. Vardi

Publication date: 4 April 2008

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

Full work available at URL: https://doi.org/10.1007/978-3-540-69738-1_10

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Graph-Based Algorithms for Boolean Function Manipulation
• Symbolic model checking: \(10^{20}\) states and beyond
• Temporal logic can be more expressive
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Reasoning about infinite computations
• The complementation problem for Büchi automata with applications to temporal logic
• Model checking of safety properties
• Weak alternating automata are not that weak
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation
• Theories of automata on \(\omega\)-tapes: a simplified approach
• Formal Methods in Computer-Aided Design
• Model Checking Software
• Liveness checking as safety checking for infinite state spaces
• Concepts of Automata Construction from LTL
• A new heuristic for bad cycle detection using BDDs
• From linear time to branching time
• Computer Aided Verification
• Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata
• Correct Hardware Design and Verification Methods
• Tools and Algorithms for the Construction and Analysis of Systems
• BÜCHI COMPLEMENTATION MADE TIGHTER
• Lower Bounds for Complementation of ω-Automata Via the Full Automata Technique
• Cluster-Based LTL Model Checking of Large Systems

Cited In (32)

• Title not available (Why is that?)
• Title not available (Why is that?)
• The complexity of synchronizing Markov decision processes
• An explicit transition system construction approach to LTL satisfiability checking
• Symmetry and partial order reduction techniques in model checking Rebeca
• Automated Termination in Model Checking Modulo Theories
• Büchi Complementation and Size-Change Termination
• Finite Models vs Tree Automata in Safety Verification
• An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking
• Model-Checking First-Order Logic: Automata and Locality
• Automated formal analysis and verification: an overview
• On Model Checking for Visibly Pushdown Automata
• Linear-Time Model Checking: Automata Theory in Practice
• Transformation from PLTL to automata via NFGs
• State Coverage Metrics for Specification-Based Testing with Büchi Automata
• Automata-driven partial order reduction and guided search for LTL model checking
• Linear temporal logic -- from infinite to finite horizon
• From Monadic Logic to PSL
• Linear temporal logic symbolic model checking
• Mediating for reduction (on minimizing alternating Büchi automata)
• Formal Approaches to Software Testing
• State of Büchi Complementation
• LTL under reductions with weaker conditions than stutter invariance
• From Philosophical to Industrial Logics
• Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition
• Automated Technology for Verification and Analysis
• On-the-fly Emptiness Check of Transition-Based Streett Automata
• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
• The design of checkable automata. II
• SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
• Generalizations of checking stack automata: characterizations and hierarchies
• Model Checking Using Generalized Testing Automata

This page was built for publication: Automata-Theoretic Model Checking Revisited

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