Improved automata generation for linear temporal logic
From MaRDI portal
Recommendations
- Improving automata generation for linear temporal logic by considering the automaton hierarchy
- Efficient Büchi automata form LTL formulae
- Implementation and Application of Automata
- Experiments with deterministic -automata for formulas of linear temporal logic
- scientific article; zbMATH DE number 6401143
Cited in
(32)- Tool support for learning Büchi automata and linear temporal logic
- An abstraction-refinement methodology for reasoning about network games
- An explicit transition system construction approach to LTL satisfiability checking
- A symbolic decision procedure for symbolic alternating finite automata
- Transformation from PLTL to automata via NFGs
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- From LTL to deterministic automata. A safraless compositional approach
- GSTE is partitioned model checking
- Optimized temporal monitors for SystemcC
- More efficient on-the-fly LTL verification with Tarjan's algorithm
- On the relationship between LTL normal forms and Büchi automata
- A logical approach to data-aware automated sequence generation
- Improving automata generation for linear temporal logic by considering the automaton hierarchy
- Büchi Store: an open repository of Büchi automata
- Inference rules in multi-agents' temporal logics
- Model checking probabilistic systems
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- Logic programming approach to automata-based decision procedures
- Towards a notion of unsatisfiable and unrealizable cores for LTL
- Linear temporal logic symbolic model checking
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
- GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
- Incremental reasoning on monadic second-order logics with logic programming
- From linear temporal logics to Büchi automata: the early and simple principle
- Rules admissible in transitive temporal logic \(\mathrm{T}_{\mathrm{S}4}\), sufficient condition
- Bridging the gap between single- and multi-model predictive runtime verification
- The effects of semantic simplifications on random \textit{BST}-like expression-trees
- Absorbing patterns in BST-like expression-trees
- Tableau-based automata construction for dynamic linear time temporal logic
- Branching time logics \(\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha }\) with operations \textit{Until} and \textit{Since} based on bundles of integer numbers, logical consecutions, deciding algorithms
- Linear temporal logic with until and next, logical consecutions
- Reasoning about XML with temporal logics and automata
This page was built for publication: Improved automata generation for linear temporal logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4817549)
