About the temporal logic of the lexicographic products of unbounded dense linear orders: a new study of its computability

Philippe Balbiani (1, 2)

1 IRIT-LILaC - Logique, Interaction, Langue et Calcul
2 CNRS - Centre National de la Recherche Scientifique

This article considers the temporal logic of the lexicographic products of unbounded dense linear orders and provides via mosaics a new proof of the membership in NP of the satisfiability problem it gives rise to.

Mots clés: Linear temporal logic; lexicographic product; satisfiability problem; decidability; complexity; mosaic method; decision procedure

Domaines: Logique en informatique [cs.LO]

Philippe Balbiani. About the temporal logic of the lexicographic products of unbounded dense linear orders: a new study of its computability. International Workshop on Logic and Cognition (WOLC 2016), Dec 2016, Canton, China. ⟨hal-02936481⟩