Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: A∪B holds at the current time instant w iff either B holds at w or there exists a time instant w' in the future at which B holds and such that A holds in all the time instants between the current one and ẃ. This “ambivalent” nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in (...) contrast, we make explicit this duality of until by introducing a new temporal operator ∇ that allows us to formalize the “history” of until, i.e., the “internal” universal quantification over the time instants between the current one and ẃ. This approach provides the basis for formalizing deduction systems for temporal logics endowed with the until operator. For concreteness, we give here a labeled natural deduction system N(LTL∇) for a linear-time logic LTL∇ endowed with the new history operator. We show that LTL∇ is equivalent to the linear temporal logic LTL with until, which follows by formalizing back and forth translations between the two logics. We also define an indirect translation from LTL∇ into LTL via temporal logics with past operators; such a result provides an upper bound to the problem of satisfiability for LTL∇ formulas. (shrink)

Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: A∪B holds at the current time instant w iff either B holds at w or there exists a time instant w' in the future at which B holds and such that A holds in all the time instants between the current one and ẃ. This “ambivalent” nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in (...) contrast, we make explicit this duality of until by introducing a new temporal operator ∇ that allows us to formalize the “history” of until, i.e., the “internal” universal quantification over the time instants between the current one and ẃ. This approach provides the basis for formalizing deduction systems for temporal logics endowed with the until operator. For concreteness, we give here a labeled natural deduction system N(LTL∇) for a linear-time logic LTL∇ endowed with the new history operator. We show that LTL∇ is equivalent to the linear temporal logic LTL with until, which follows by formalizing back and forth translations between the two logics. We also define an indirect translation from LTL∇ into LTL via temporal logics with past operators; such a result provides an upper bound to the problem of satisfiability for LTL∇ formulas. (shrink)

We present an extension of the mosaic method aimed at capturing many-dimensional modal logics. As a proof-of-concept, we define the method for logics arising from the combination of linear tense operators with an “orthogonal” S5-like modality. We show that the existence of a model for a given set of formulas is equivalent to the existence of a suitable set of partial models, called mosaics, and apply the technique not only in obtaining a proof of decidability and a proof of completeness (...) for the corresponding Hilbert-style axiomatization, but also in the development of a mosaic-based tableau system. We further consider extensions for dealing with the case when interactions between the two dimensions exist, thus covering a wide class of bundled Ockhamist branching-time logics, and present for them some partial results, such as a non-analytic version of the tableau system. (shrink)