A History of Until

Details A History of Until A History of Until

2009-10-23

arxiv.org/abs/0910.4500v2

Computer Science

Logic in Computer Science

24 pages, full version of paper at Methods for Modalities 2009 (M4M-6)

Scientific paper

Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: A until 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 w'. 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 to provide well-behaved natural deduction rules for linear-time logics 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 w'. 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 for a linear-time logic endowed with the new operator and show that, via a proper translation, such a system is also sound and complete with respect to the linear temporal logic LTL with until.

Affiliated with

Also associated with

No associations

Rating

A History of Until does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with A History of Until, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A History of Until will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-423631