LTL2BA

swMATH10956MaRDI QIDQ22908

No author found.

Related Items

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

This page was built for software: LTL2BA