Manipulating LTL Formulas Using Spot 1.0
From MaRDI portal
Publication:5166705
DOI10.1007/978-3-319-02444-8_31zbMATH Open1410.68223OpenAlexW35895474MaRDI QIDQ5166705FDOQ5166705
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
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
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Cited In (13)
- LTL to self-loop alternating automata with generic acceptance and back
- From Spot 2.0 to Spot 2.10: What’s New?
- Decentralized route-planning for multi-vehicle teams to satisfy a subclass of linear temporal logic specifications
- From LTL to unambiguous Büchi automata via disambiguation of alternating automata
- Efficient approach of translating LTL formulae into Büchi automata
- Markov chains and unambiguous automata
- Modified ant colony algorithm for constructing finite state machines from execution scenarios and temporal formulas
- Generic Emptiness Check for Fun and Profit
- New Optimizations and Heuristics for Determinization of Büchi Automata
- 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
Uses Software
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)
