Deterministic generators and games for Ltl fragments

DOI10.1145/963927.963928zbMath1366.03181OpenAlexW2178626170MaRDI QIDQ5277690

Salvatore La Torre, Rajeev Alur

Publication date: 12 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://repository.upenn.edu/cis_papers/15

zbMATH Keywords

automatatemporal logicgames

Mathematics Subject Classification ID

Games involving graphs (91A43) Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44)

Related Items

From LTL to deterministic automata. A safraless compositional approach ⋮ Graph Games and Reactive Synthesis ⋮ Compositional and symbolic synthesis of reactive controllers for multi-agent systems ⋮ Linear temporal logic -- from infinite to finite horizon ⋮ Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition ⋮ Automata-theoretic decision of timed games ⋮ Robust, expressive, and quantitative linear temporal logics: pick any two for free ⋮ Index appearance record with preorders ⋮ Cooperative concurrent games ⋮ Finding and fixing faults ⋮ On the complexity of rational verification ⋮ Certified reinforcement learning with logic guidance ⋮ Agent planning programs ⋮ Harmonization of interacting automata ⋮ On tolerance of discrete systems with respect to transition perturbations ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ Synthesis of Reactive(1) designs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Index Appearance Record for Transforming Rabin Automata into Parity Automata ⋮ Optimal Translation of LTL to Limit Deterministic Automata ⋮ A GENERAL NOTION OF UNIFORM STRATEGIES ⋮ Problems of synthesis of \(\Sigma\)-automata specified in languages LP and LF of first order logic ⋮ Visibly pushdown modular games ⋮ Doomsday equilibria for omega-regular games ⋮ Most General Property-Preserving Updates ⋮ Cycle detection in computation tree logic ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ Static and dynamic property-preserving updates ⋮ Complexity of model checking MDPs against LTL specifications

This page was built for publication: Deterministic generators and games for Ltl fragments