LTL2BA
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Tool support for learning Büchi automata and linear temporal logic
- MCGP
- DeepSynth
- FoCs
- PROD
- SPIN
- POEM
- Maria
- NuSMV
- LiQuor
- Efficient approach of translating LTL formulae into Büchi automata
- On clock-aware LTL parameter synthesis of timed automata
- Punf
- CUDD
- Safraless LTL synthesis considering maximal realizability
- COMICS
- TaPAS
- Specification and verification of declarative open interaction models. A logic-based approach
- Cadence SMV
- CESAR
- SPOT
- From LTL to unambiguous Büchi automata via disambiguation of alternating automata
- DiPro
- Path planning for robotic teams based on LTL specifications and Petri net models
- BEEM
- LTL to self-loop alternating automata with generic acceptance and back
- Casaal
- Automated temporal equilibrium analysis: verification and synthesis of multi-player games
- LTLCon
- From LTL to deterministic automata. A safraless compositional approach
- Model checking of pushdown systems for projection temporal logic
- Unfoldings: A partial-order approach to model checking.
- Temporal property verification as a program analysis task
- PRALINE
- More efficient on-the-fly LTL verification with Tarjan's algorithm
- LTL receding horizon control for finite deterministic systems
- On the relationship between LTL normal forms and Büchi automata
- The Maude LTL model checker
- Analyzing LTL model checking techniques for plan synthesis and controller synthesis (work in progress)
- Comparison of algorithms for checking emptiness on Büchi automata
- Mediating for reduction (on minimizing alternating Büchi automata)
- Automata and temporal logic over arbitrary linear time
- Improving automata generation for linear temporal logic by considering the automaton hierarchy
- Büchi Store: an open repository of Büchi automata
- Unbeast: Symbolic Bounded Synthesis
- scientific article; zbMATH DE number 1799521 (Why is no real title available?)
- Towards SAT-based BMC for LTLK over interleaved interpreted systems
- 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
- Java-MaC
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- ProbReach
- Antichains
- Degeneralization algorithm for generation of Büchi automata based on contented situation
- ltl2dstar
- Rabinizer
- New optimizations and heuristics for determinization of Büchi automata
- Approximate automata for omega-regular languages
- GOAL
- Translating Testing Theories for Concurrent Systems
- Extending co-logic programs for branching-time model checking
- Rabinizer 3: Safraless translation of LTL to small deterministic automata
- Logic programming approach to automata-based decision procedures
- Model Checking Temporal Metric Specifications with Trio2Promela
- From Philosophical to Industrial Logics
- Model Checking LTL Formulae in RAISE with FDR
- Antichains for the Automata-Based Approach to Model-Checking
- On-the-fly emptiness check of transition-based Streett automata
- Acacia+
- Minimal counterexamples for linear-time probabilistic verification
- LTL_to_DRA
- lbtt
- SReachTools
- EAGLE
- Program-Conflict-Analysis
- MSO_Regex_Equivalence
- Copilot
- TXP
- scientific article; zbMATH DE number 1973989 (Why is no real title available?)
- scientific article; zbMATH DE number 1982196 (Why is no real title available?)
- scientific article; zbMATH DE number 1982198 (Why is no real title available?)
- scientific article; zbMATH DE number 1982203 (Why is no real title available?)
- scientific article; zbMATH DE number 1982209 (Why is no real title available?)
- libVATA
- WPDS++
- Symbolic bounded synthesis
- scientific article; zbMATH DE number 1796123 (Why is no real title available?)
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- Rabinizer: small deterministic automata for \({\mathrm{LTL}(\mathrm{F},\mathrm{G})}\)
- Baselines
- Linear temporal logic symbolic model checking
- scientific article; zbMATH DE number 2176483 (Why is no real title available?)
- Runtime verification using the temporal description logic \(\mathcal{ALC}\)-LTL revisited
- Model Checking Using Generalized Testing Automata
- The Linear Temporal Logic of Rewriting Maude Model Checker
- A compositional automata-based semantics and preserving transformation rules for testing property patterns
- Minimization and canonization of GFG transition-based automata
- Component-wise incremental LTL model checking
This page was built for software: LTL2BA
