Manipulating LTL Formulas Using Spot 1.0

DOI10.1007/978-3-319-02444-8_31zbMath1410.68223OpenAlexW35895474MaRDI QIDQ5166705

Alexandre Duret-Lutz

Publication date: 8 July 2014

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-02444-8_31

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

Decentralized route-planning for multi-vehicle teams to satisfy a subclass of linear temporal logic specifications, From LTL to deterministic automata. A safraless compositional approach, Efficient approach of translating LTL formulae into Büchi automata, From LTL to unambiguous Büchi automata via disambiguation of alternating automata, Modified ant colony algorithm for constructing finite state machines from execution scenarios and temporal formulas, Time window temporal logic, Markov chains and unambiguous automata, LTL to self-loop alternating automata with generic acceptance and back, New Optimizations and Heuristics for Determinization of Büchi Automata, Generic Emptiness Check for Fun and Profit, A compositional automata-based semantics and preserving transformation rules for testing property patterns

Uses Software

• SPIN
• SPOT
• ltlcross
• autcross
• LBT
• lbtt
• ltlfilt