Manipulating LTL Formulas Using Spot 1.0

DOI10.1007/978-3-319-02444-8_31MaRDI QIDQ5166705zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Modifying LOTOS specifications by means of automatable formula-based integrations
• Model Checking Software
• scientific article; zbMATH DE number 1948409
• A Logic Approach for LTL System Modification
• Model checking LTL using constraint programming
• Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications

Cited in

(13)

• LTL to self-loop alternating automata with generic acceptance and back
• Decentralized route-planning for multi-vehicle teams to satisfy a subclass of linear temporal logic specifications
• From Spot 2.0 to Spot 2.10: What’s New?
• From LTL to unambiguous Büchi automata via disambiguation of alternating automata
• Efficient approach of translating LTL formulae into Büchi automata
• New optimizations and heuristics for determinization of Büchi automata
• Generic emptiness check for fun and profit
• Markov chains and unambiguous automata
• Modified ant colony algorithm for constructing finite state machines from execution scenarios and temporal formulas
• A compositional automata-based semantics and preserving transformation rules for testing property patterns
• Time window temporal logic
• From LTL to deterministic automata. A safraless compositional approach
• From LTL to unambiguous Büchi automata via disambiguation of alternating automata

Describes a project that uses

Uses Software

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

This page was built for publication: Manipulating LTL Formulas Using Spot 1.0

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5166705)