LTL2BA

swMATH10956MaRDI QIDQ22908FDOQ22908

Author name not available (Why is that?)

Cited In (94)

• From LTL to Symbolically Represented Deterministic Automata
• Hybrid Systems: Computation and Control
• Minimal counterexamples for linear-time probabilistic verification
• Decidability of LTL for vector addition systems with one zero-test
• Comparison of algorithms for checking emptiness on Büchi automata
• Linear Encodings of Bounded LTL Model Checking
• Model Checking Software
• LTL to self-loop alternating automata with generic acceptance and back
• Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
• Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
• Unfoldings: A partial-order approach to model checking.
• Verifying a signature architecture: a comparative case study
• Extending Co-logic Programs for Branching-Time Model Checking
• Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic
• The Linear Temporal Logic of Rewriting Maude Model Checker
• Model Checking LTL Formulae in RAISE with FDR
• The Maude LTL model checker
• Towards SAT-based BMC for LTLK over Interleaved Interpreted Systems
• Efficient approach of translating LTL formulae into Büchi automata
• Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata
• Theorem Proving in Higher Order Logics
• Title not available (Why is that?)
• Automata Theory and Model Checking
• Temporal property verification as a program analysis task
• GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
• Computer Aided Verification
• Symbolic bounded synthesis
• Applications and Theory of Petri Nets 2004
• Computer Aided Verification
• On clock-aware LTL parameter synthesis of timed automata
• Simulation relations for alternating Büchi automata
• Automated temporal equilibrium analysis: verification and synthesis of multi-player games
• The mu-calculus and Model Checking
• Title not available (Why is that?)
• Rabinizer: Small Deterministic Automata for LTL(F,G)
• Specification and verification of declarative open interaction models. A logic-based approach
• Concepts of Automata Construction from LTL
• Tools and Algorithms for the Construction and Analysis of Systems
• Mathematical Foundations of Computer Science 2003
• Linear temporal logic symbolic model checking
• Runtime verification using the temporal description logic \(\mathcal{ALC}\)-LTL revisited
• Büchi Store: an open repository of Büchi automata
• A canonical form based decision procedure and model checking approach for propositional projection temporal logic
• Title not available (Why is that?)
• Translating Testing Theories for Concurrent Systems
• Mediating for reduction (on minimizing alternating Büchi automata)
• Mediating for reduction (on minimizing alternating Büchi automata)
• Tool support for learning Büchi automata and linear temporal logic
• Graph Games and Reactive Synthesis
• Improved Algorithms for the Automata-Based Approach to Model-Checking
• Title not available (Why is that?)
• Approximate Automata for Omega-Regular Languages
• Safraless LTL synthesis considering maximal realizability
• Title not available (Why is that?)
• Improving automata generation for linear temporal logic by considering the automaton hierarchy
• From Philosophical to Industrial Logics
• Logic programming approach to automata-based decision procedures
• Antichains for the Automata-Based Approach to Model-Checking
• Automata and temporal logic over arbitrary linear time
• Title not available (Why is that?)
• A compositional automata-based semantics and preserving transformation rules for testing property patterns
• Degeneralization algorithm for generation of Büchi automata based on contented situation
• Model Checking Temporal Metric Specifications with Trio2Promela
• Computer Aided Verification
• Analog property checkers: a DDR2 case study
• From LTL to deterministic automata. A safraless compositional approach
• Title not available (Why is that?)
• Title not available (Why is that?)
• Component-wise incremental LTL model checking
• On the Relationship between LTL Normal Forms and Büchi Automata
• Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
• LTL receding horizon control for finite deterministic systems
• Parametric linear dynamic logic
• The modeling library of eavesdropping methods in quantum cryptography protocols by model checking
• More efficient on-the-fly LTL verification with Tarjan's algorithm
• A constraint-based approach to solving games on infinite graphs
• Unbeast: Symbolic Bounded Synthesis
• Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words
• Model Checking Using Generalized Testing Automata
• Model checking of pushdown systems for projection temporal logic
• Title not available (Why is that?)
• From LTL to unambiguous Büchi automata via disambiguation of alternating automata
• On-the-fly emptiness check of transition-based Streett automata
• Implementation and Application of Automata
• Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment
• Incremental reasoning on monadic second-order logics with logic programming
• Coinductive Algorithms for Büchi Automata
• Theorem Proving in Higher Order Logics
• Title not available (Why is that?)
• New Optimizations and Heuristics for Determinization of Büchi Automata
• Path planning for robotic teams based on LTL specifications and Petri net models
• Title not available (Why is that?)
• Analyzing LTL model checking techniques for plan synthesis and controller synthesis (work in progress)
• An Automata View to Goal-Directed Methods

This page was built for software: LTL2BA