SPOT
From MaRDI portal
SPOT Q21456
Cited in
(only showing first 100 items - show all)- JBDD
- Transition_Systems_and_Automata
- Reactive synthesis with maximum realizability of linear temporal logic specifications
- LTL model checking with Neco
- New optimizations and heuristics for determinization of Büchi automata
- Generic emptiness check for fun and profit
- From LTL and limit-deterministic Büchi automata to deterministic parity automata
- BoSy
- Delag
- A logical approach to data-aware automated sequence generation
- Time window temporal logic
- Path planning for robotic teams based on LTL specifications and Petri net models
- Good-for-MDPs automata for probabilistic analysis and reinforcement learning
- scientific article; zbMATH DE number 7455737 (Why is no real title available?)
- scientific article; zbMATH DE number 7455747 (Why is no real title available?)
- Automata-driven partial order reduction and guided search for LTL model checking
- On-the-fly emptiness check of transition-based Streett automata
- From LTL to unambiguous Büchi automata via disambiguation of alternating automata
- Index appearance record with preorders
- Determinization and limit-determinization of Emerson-Lei automata
- Live synthesis
- Semantic labelling and learning for parity game solving in LTL synthesis
- Index appearance record for transforming Rabin automata into parity automata
- A weakness measure for GR(1) formulae
- Strategies, model checking and branching-time properties in Maude
- Unbeast
- Manipulating LTL Formulas Using Spot 1.0
- Linear temporal logic symbolic model checking
- Seminator 2 can complement generalized Büchi automata via improved semi-determinization
- Decentralized route-planning for multi-vehicle teams to satisfy a subclass of linear temporal logic specifications
- Practical synthesis of reactive systems from LTL specifications via parity games
- 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
- Leviathan
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- A tableau construction for finite linear-time temporal logic
- An explicit transition system construction approach to LTL satisfiability checking
- From LTL to deterministic automata. A safraless compositional approach
- Timed hyperproperties
- Rabinizer 3: Safraless translation of LTL to small deterministic automata
- On the relationship between LTL normal forms and Büchi automata
- A CTL* Model Checker for Petri Nets
- FoCs
- SPIN
- DiVinE
- Maria
- NuSMV
- CUDD
- MONA
- Colt
- LTSmin
- iFEST
- jSpin
- Cadence SMV
- neco-spot
- Neco
- SNAKES
- BEEM
- Omega+
- PackUp
- STeLP
- NMRDPP
- LTL2BA
- ABC
- PGSolver
- ORME
- RATSY
- MuACOsm
- nuXmv
- ltl2dstar
- Rabinizer
- FuncTion
- LTLAutomizer
- ModelPlex
- Ultimate
- Acacia+
- Datalog LITE
- LTL_to_DRA
- AIGER
- Meddly
- autcross
- LBT
- lbtt
- ltlcross
- ltlfilt
- Program-Conflict-Analysis
- Strix
- Baselines
- MultiGain
- ltl3tela
- Pecan
- Boolean_Expression_Checkers
- VIS
- LTL to self-loop alternating automata with generic acceptance and back
- ROSMonitoring
- Safraless LTL synthesis considering maximal realizability
- One theorem to rule them all: a unified translation of LTL into \(\omega \)-automata
- Owl
- Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations
- From Philosophical to Industrial Logics
This page was built for software: SPOT
