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.