Abstract
Constraint lineartime 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 (ℤ, < , =), the domain of integers with order and equality. We prove that over (ℤ, < , =), 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 singlesided games.
BibTeX  Entry
@InProceedings{bhaskar_et_al:LIPIcs.TIME.2022.8,
author = {Bhaskar, Ashwin and Praveen, M.},
title = {{Realizability Problem for Constraint LTL}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {8:18:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772624},
ISSN = {18688969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/17255},
URN = {urn:nbn:de:0030drops172556},
doi = {10.4230/LIPIcs.TIME.2022.8},
annote = {Keywords: Realizability, constraint LTL, Strategy trees, Tree automata}
}
Keywords: 

Realizability, constraint LTL, Strategy trees, Tree automata 
Collection: 

29th International Symposium on Temporal Representation and Reasoning (TIME 2022) 
Issue Date: 

2022 
Date of publication: 

29.10.2022 