oguz@herky.cs.uiowa.edu (01/18/91)
In <3747@ns-mx.uiowa.edu> I posted the following query:
Is anybody aware of a temporal logic with "bounded" modalities? This logic would
have the modality F_m for each natural number m, instead of the usual eventuality
operator F so that "F_m p" would mean "within m units of time from the present
time p will hold true". Similarly, "G_m p" would mean "henceforth throughout m units
of time p will hold true".
The following is a summary of replies that I have received. I am grateful
to all those who replied. All the replies were quite helpful for me.
-- Halit Oguztuzun
From: jonathan@yetti.cs.yorku.ca (Jonathan Ostroff)
Message-Id: <9012300217.AA26297@yetti.yorku.ca>
For real-time temporal logic (not exactly what you asked for) consult
IEEE Trans. on Parallel & Distr. Systems, April 1990, p170-183,
"Deciding properties of timed transition models".
From: D Jayasimha <jayasim@cis.ohio-state.edu>
Message-Id: <9012302222.AA01845@platypus.cis.ohio-state.edu>
We (Prof. Nachum Dershowitz and I) have worked on something very close
to what you ask in your query. We have defined the concept of
"Bounded Fairness" and defined a temporal operator to describe the behavior,
and investigated some properties of this logic. We have defined the notion
of boundedness in terms of "occurrence of an event" than in terms of time to
make the notion general. Here's an informal description of "k-boundedness"
followed by an abstract. The details of the Tech. Rpt. that we have on this
subject is given at the end.
In real-time applications, for example, the weak commitment of eventual
occurrence may not be sufficient. An application might require that
any process $p sub i$ which requests a resource (such as a critical region) be
granted the resource within the next k (k >=1) times that
the resource is granted to any process arriving after $p sub i$. This
is a stronger requirement relating the frequency of shared
resource access of a particular process with regard to other processes
(which access the resource with mutual exclusion). This, essentially,
is the notion of k-bounded fairness. This idea of k-bounded
fairness is elegant because we are able to express a variety of fairness
notions: k=1 corresponds to the first come first served (FCFS)
discipline (which may be too restrictive), and k = infinity corresponds to
the (totally unrestricted) eventuality concept. Note that this idea of
bounded fairness, though suited to real-time applications, does not make any
assumption about the relative progress of processes; i.e., a process' execution
rate on a processor is independent of the execution rate of another process.
Such an assumption would make our solutions not only restrictive, but
time-dependent too.
A scheduler q is k-bounded fair if a process $p sub i$ wanting to enter its
critical region is \fIguaranteed\fP to do so at one of the next \fIk\fP times
that $q$ schedules either $p sub i$ or a process arriving after $p sub i$.
ABSTRACT
In this paper we study bounded fairness. Bounded fairness is stronger
than the usual notion of fairness based on the temporal concept of eventuality.
We formalize bounded fairness by introducing a new binary operator k into
temporal logic. The syntax, semantics, and an axiom system for this new logic
kTL are given. This logic is shown to be more powerful than the temporal logic
with the eventuality operator, and as powerful as the logic with the until
operator. We show that kTL is complete and satisfiable.
We also give applications of the bounded fairness concept: we specify
bounded fairness requirements for standard concurrent programming
problems, and we show, for example, that Dekker's mutual exclusion algorithm is
fair in the conventional sense, but not bounded fair. We also give examples of
bounded fair algorithms.
"Bounded Fairness," D. N. Jayasimha, Nachum Dershowitz, CSRD TR No. 615,
Center for Supercomputing Res. & Dev., Univ. of Illinois, Urbana, IL 61801.
Dec. 1986.
From: Lenore Zuck <zuck-lenore@CS.YALE.EDU>
Message-Id: <9012302331.AA20025@thailand.CS.YALE.EDU>
I am not aware of any work that directly discusses bounded TL, however, at
least the bounded eventaully is easily expressible in 'current' terms by the
next operator, that is, your F_m p seems to be exactly X^m p, where X is the
(strict) next operator. Note that X^m p implies that there is an instance
which is k steps from now. If you are dealing with models which could be
finite, you might want to use the 'weak next' operator (if you are
interested, I can give you several references to these operators). Your G_m
p operator is also expressible in the classical TL, only not as neatly as
before. Here, if you are dealing with finite models, you should definitely
use the weak next (say, W) operator, and G_m p is a conjuction of i,
i=0,...,m, of W^i p. If the models are infinte (to the future), then replace
the W with X.
[F_m p must be the disjunction of i,i=0,...,m of W^i p. See next respondent.]
From: Lenore Zuck <zuck-lenore@CS.YALE.EDU>
Message-Id: <9101011601.AA01250@thailand.CS.YALE.EDU>
The weak next operator appears in most papers that discuss the past operators.
Some of these (in a bibtex format) are:
@inproceedings{LP,
author = {O. Lichtenstein and A. Pnueli},
title = {Checking that Finite-State Concurrent Programs
Satisfy their Linear Specifications},
booktitle = popl12,
year = 1985,
pages = {97--107}
}
@inproceedings{LPZ,
author = {O. Lichtenstein and A. Pnueli and L. Zuck},
title = {The Glory of the Past},
booktitle = lop, % workshop on ligcs of programs, LNCS xxx
year = 1985,
pages = {196--218}
}
@inproceedings{ManPnu,
author = {Zohar Manna and Amir Pnueli},
title = {The anchored version of temporal Logic},
booktitle={LNCS 354},
year=1989, % I am not sure about the year, my guess is 89
pages={201--284}}
In addition, I think that in the Proceedings of the first LICS (1986), both
Pnueli-Zuck and Vardi-Wolper refer to the weak next operator.
From: yodaiken%chelm@cs.umass.edu (victor yodaiken)
Message-Id: <9101021600.AA11589@chelm.cs.umass.edu>
Any temporal logic with the Next operator fits the bill.
Diamond P is simply (Exists n) Next^n P and Box P is
(forall n)Next^n P . A bounded logic is obtained by simply forbidding
unbounded quantification over Next.
You may also be interested in my work on the modal arithmetic. I use
the pumping lemma of regular languages to get analogs of the unbounded
t.l. out of bounded formalism. That is, inthe arithmetic we have
a boolean function Enable(u) which has value 1 iff u is a sequence
of transition labels denoting an enabled path in the state machine
which originates at the current state. We also have a functional
(after u) so that (after u)f(x) is a boolean function which has value
1 iff f(x)>0 in the state reached by following u from the current state.
Thus, Always f(x) is defined to be (forall u)(Enable(u) -> (after u)f(x)).
Since the interpretation of these terms is over finite automata, we can show
that this is equivalent to a bounded expression.
We can also build finer expressions such as "Any path containing k
or fewer 'a' transitions must visit a state where f(x)>0" etc.
I'll send you some tech reports if you want.
From: Thomas Henzinger <tah@Theory.Stanford.EDU>
Message-Id: <9101021924.AA19904@Baal.Stanford.EDU>
R. Alur and T. Henzinger study such a logic ("metric temporal logic")
in "Real-time Logics: Complexity and Expressiveness" (appeared at
LICS 1990). More references can be found there.
From: rar@ads.com (Bob Riemenschneider)
Message-Id: <9101022148.AA07232@saturn.ads.com>
I'm pretty sure van Benthem treats them in _The Logic of Time_. If I
remember correctly, he points out that they're of limited interest
since -- once you throw in a bit of arithmetic on the indices -- the
logic is undecidable, and so you might as well use a first-order logic
with time points.
From: Jack Campin <jack@cs.glasgow.ac.uk>
Message-Id: <27606.9101031505@crete.cs.glasgow.ac.uk>
Something like that is described in Rescher & Urquhart's "Temporal Logic".
From: hearne@unicorn.cc.wwu.edu (Jim Hearne)
Message-Id: <9101032105.AA03906@unicorn.cc.wwu.edu>
A colleague of mine ( Prof. Geoff Matthews ) and developed such a logic
in the course of providing foundations for an event oriented programming
language called Tahiti. Our version dealt only with discrete times
(non-discrete times seemed to have decidibility problems). We did not
explore the logic in much detail, but the operators you refer to are
part of the Tahiti language (so one can branch on both past and future
temporaly qualified conditions).
From: hearne@unicorn.cc.wwu.edu (Jim Hearne)
Message-Id: <9101030109.AA18168@unicorn.cc.wwu.edu>
[...] Incidentally, the Tahiti
language is equiped with the quantified temporal operators
so programmers can say things like
if such-and-such has happened in the last five seconds then
do such-and-such
end if
or
if such-and-such remains true continuously for the next three seconds then
do such-and-such
end if
From: hearne@unicorn.cc.wwu.edu (Jim Hearne)
Message-Id: <9101142359.AA23684@unicorn.cc.wwu.edu>
There are four papers on Tahiti. The last one is
the most helpful:
``Possible Worlds Computing on a Hypercube'' with
Debra Jusak in Proceedings of the International Conference
on iPSC, August, Irvine, California.
``How to Use Up Processors,'' with Debra Jusak,
Proceedings of the Frontiers 90 Conference on Massively
Parallel Computation, College Park Maryland, October 1990.
``Language and Run-time Support for Event Programming in
a Distributed Environment'', with Debra Jusak, Proceedings of
the Conference on Future Trends in Distributed Computing
``The Tahiti Programming Language: Events as First-Class
Objects,'' with Debra Jusak,
Proceedings of the 1990 International Conference on
Computer Languages, New Orleans.
From: 6500ramk%ucsbuxa@hub.ucsb.edu (Y S Ramakrishna)
Message-Id: <9101032042.AA21916@ucsbuxa.ucsb.edu>
You might find the following references useful.
1. Emerson E A, et al, "Quantitative Temporal Reasoning", Proceedings of the
Workshop on Finite-State Concurrency, Grenoble, France, 1989.
2. Koymans, Vytopil, de Roever, "Real-time Programming & Asynchronous Message-
Passing", 10th ACM POPL, 1983.
3. Ostroff J S,"Temporal Logic of Real-Time Systems", PhD Thesis, Univ of
Toronto, 1987.
4. Alur R, Henzinger T, "A Really Temporal Logic", Tech Rep STAN-CS-89-1267,
Stanford University, 1989.