scientific article; zbMATH DE number 1759609
From MaRDI portal
Publication:4536600
zbMATH Open0999.68113MaRDI QIDQ4536600FDOQ4536600
Authors: Kousha Etessami, Gerard J. Holzmann
Publication date: 28 November 2002
Title of this publication is not available (Why is that?)
Recommendations
Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (38)
- Title not available (Why is that?)
- Applicability of fair simulation
- Title not available (Why is that?)
- LTL to self-loop alternating automata with generic acceptance and back
- Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic
- Dissecting \texttt{ltlsynt}
- From Spot 2.0 to Spot 2.10: What’s New?
- From LTL to unambiguous Büchi automata via disambiguation of alternating automata
- The Maude LTL model checker
- Transformation from PLTL to automata via NFGs
- Efficient State Space Reduction for Automata by Fair Simulation
- On-the-Fly Stuttering in the Construction of Deterministic ω-Automata
- Markov chains and unambiguous automata
- Title not available (Why is that?)
- Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata
- Automata-Theoretic Model Checking Revisited
- Büchi Store: an open repository of Büchi automata
- Tighter construction of tight Büchi automata
- Tool support for learning Büchi automata and linear temporal logic
- Approximate Automata for Omega-Regular Languages
- LTL under reductions with weaker conditions than stutter invariance
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Index appearance record with preorders
- Effective reductions of Mealy machines
- New Optimizations and Heuristics for Determinization of Büchi Automata
- Title not available (Why is that?)
- Mechanizing the Powerset Construction for Restricted Classes of ω-Automata
- Title not available (Why is that?)
- From LTL to deterministic automata. A safraless compositional approach
- Bridging the gap between single- and multi-model predictive runtime verification
- Explicit-State Model Checking
- Simulation relations and applications in formal methods
- Title not available (Why is that?)
- On the Relationship between LTL Normal Forms and Büchi Automata
- More efficient on-the-fly LTL verification with Tarjan's algorithm
- Organising LTL monitors over distributed systems with a global clock
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4536600)