Realizability problem for constraint LTL

DOI10.1016/J.IC.2023.105126arXiv2207.06708OpenAlexW4388968637MaRDI QIDQ6178458FDOQ6178458

Authors: Ashwin Bhaskar, M. Praveen 

Publication date: 18 January 2024

Published in: Information and Computation (Search for Journal in Brave)

Abstract: Constraint linear-time temporal logic (CLTL) is an extension of LTL that is interpreted on sequences of valuations of variables over an infinite domain. The atomic formulas are interpreted as constraints on the valuations. The atomic formulas can constrain valuations over a range of positions along a sequence, with the range being bounded by a parameter depending on the formula. The satisfiability and model checking problems for CLTL have been studied by Demri and D'Souza. We consider the realizability problem for CLTL. The set of variables is partitioned into two parts, with each part controlled by a player. Players take turns to choose valuations for their variables, generating a sequence of valuations. The winning condition is specified by a CLTL formula -- the first player wins if the sequence of valuations satisfies the specified formula. We study the decidability of checking whether the first player has a winning strategy in the realizability game for a given CLTL formula. We prove that it is decidable in the case where the domain satisfies the completion property, a property introduced by Balbiani and Condotta in the context of satisfiability. We prove that it is undecidable over $(mathbbZ,<,=)$, the domain of integers with order and equality. We prove that over $(mathbbZ,<,=)$, it is decidable if the atomic constraints in the formula can only constrain the current valuations of variables belonging to the second player, but there are no such restrictions for the variables belonging to the first player. We call this single-sided games.

Full work available at URL: https://arxiv.org/abs/2207.06708

zbMATH Keywords

realizabilitytree automataconstraint LTLstrategy trees

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites Work

• Infinite Games
• A really temporal logic
• An automata-theoretic approach to constraint LTL
• Automata, logics, and infinite games. A guide to current research
• LTL with the freeze quantifier and register automata
• Two-variable logic on data words
• Reactive synthesis from interval temporal logic specifications
• Title not available (Why is that?)
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• Finite-memory automata
• The complementation problem for Büchi automata with applications to temporal logic
• From liveness to promptness
• Verification, Model Checking, and Abstract Interpretation
• Solving parity games on integer vectors
• Title not available (Why is that?)
• Computer Science Logic
• Decidable Extensions of Church’s Problem
• Temporal logics of repeating values
• Dynamic controllability of simple temporal networks with uncertainty: simple rules and fast real-time execution
• Synthesis of data word transducers
• Parameterized synthesis for fragments of first-order logic over data words
• Reasoning about data repetitions with counter systems
• Nondeterministic Tree Automata
• Deciding Parity Games in Quasi-polynomial Time

This page was built for publication: Realizability problem for constraint LTL

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