SPOT

swMATH9473MaRDI QIDQ21456FDOQ21456

Author name not available (Why is that?)

Cited In (48)

• Timed hyperproperties
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations
• Optimized temporal monitors for SystemcC
• Practical synthesis of reactive systems from LTL specifications via parity games
• A tableau construction for finite linear-time temporal logic
• LTL to self-loop alternating automata with generic acceptance and back
• One theorem to rule them all: a unified translation of LTL into \(\omega \)-automata
• LTL model checking with Neco
• An explicit transition system construction approach to LTL satisfiability checking
• Decentralized route-planning for multi-vehicle teams to satisfy a subclass of linear temporal logic specifications
• A CTL* Model Checker for Petri Nets
• From LTL to unambiguous Büchi automata via disambiguation of alternating automata
• Efficient approach of translating LTL formulae into Büchi automata
• Fairness modulo theory: a new approach to LTL software model checking
• On-the-fly emptiness check of transition-based Streett automata
• 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
• Good-for-MDPs automata for probabilistic analysis and reinforcement learning
• Strategies, model checking and branching-time properties in Maude
• 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
• Automata-driven partial order reduction and guided search for LTL model checking
• Manipulating LTL Formulas Using Spot 1.0
• Linear temporal logic symbolic model checking
• Modified ant colony algorithm for constructing finite state machines from execution scenarios and temporal formulas
• A weakness measure for GR(1) formulae
• Safraless LTL synthesis considering maximal realizability
• Applications and Theory of Petri Nets 2005
• From Philosophical to Industrial Logics
• Index appearance record with preorders
• Path planning for robotic teams based on LTL specifications and Petri net models
• Title not available (Why is that?)
• 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
• Time window temporal logic
• Seminator 2 can complement generalized Büchi automata via improved semi-determinization
• A logical approach to data-aware automated sequence generation
• From LTL to deterministic automata. A safraless compositional approach
• Reactive synthesis with maximum realizability of linear temporal logic specifications
• Component-wise incremental LTL model checking
• Rabinizer 3: Safraless translation of LTL to small deterministic automata
• On the relationship between LTL normal forms and Büchi automata
• SAT-based explicit LTL reasoning and its application to satisfiability checking

This page was built for software: SPOT