Deterministic generators and games for Ltl fragments

From MaRDI portal
Publication:5277690


DOI10.1145/963927.963928zbMath1366.03181MaRDI 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


91A43: Games involving graphs

68Q45: Formal languages and automata

03D05: Automata and formal grammars in connection with logical questions

68Q60: Specification and verification (program logics, model checking, etc.)

68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)

03B44: Temporal logic


Related Items

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