rkaivola@cc.helsinki.fi (12/18/90)
Some time ago we posted a request for temporal logic tools. This is a summary of the responses we received. The summary has been organized along the categories in the original request. We have taken the liberty of omitting the responses which were just requesting to get hold of this summary, and including only the reply considered the most accurate, if we received several replies providing the same information. Contributions in some other language than English have not been included in the original, but an abbreviated translation has been provided instead. The messages in the various categories are organised chronologically. 1> temporal logic programming languages (e.g. TEMPURA, TEMPLOG, TOKIO ) Roger Hale (rwsh@cam.sri.com) writes: >TEMPURA > >The Tempura interpreter (written in C) is available from me. It was written >as a research tool, and is available at no charge (I can send it by email). >It is not particularly easy to use, though it is quite useable and efficient >if you know what you're doing. It has been run on SUN/VAX Unix and on PCs. > >One point worth emphasising is that the Tempura programming language is >a *deterministic* *subset* of Moszkowski's ITL. Disjunction, negation, >diamond, etc may not appear in programs (though they do, of course, appear >in their ITL specifications). Thomas Kropf (kropf@ira.uka.de) writes: >At our institute we are using different temporal logic approaches >for hardware verification purposes. Therefore, a year ago, we >performed a similar kind of "poll" as you are doing now. So I will >first write some words about the tools really accessible and append a >detailed email I received. > >A quite frustrating experience I made was, that a huge amount of >publications have been written concerning temporal logic but >there are nearly no implementations available. But now, what's going on: > >* temporal logic programming languages: > The only implementation really available for us has been programmed > at our university by Christoph Brzoska. It is based on TEMPLOG, first > presented by Abadi and Manna on LICS 86. The interpreter is written > in KA-Prolog, their own Prolog implementation. I do not know, whether > it would be distributed outside our university, but for further in- > formations contact: Christoph Brzoska <brzoska@ira.uka.de>, > Institut fuer Logik, Komplexitaet und Deduktionssysteme, Universitaet > Karlsruhe, PO-Box 6980, 7500 Karlsruhe, Germany. Christoph Brzoska (broszka@ira.uka.de) writes (a translation from German): >... a student of mine has implemented a meta-interpreter for the temporal >language TEMPLOG. The interpreter is implemented in KA-Prolog, a dialect of >Prolog developed in Karlsruhe. The implemented system has been used in >the verification of some hardware-examples. On the basis of this it can >be said that the system is very suitable for modelling hardware and >concurrent processes, e.g. it is relatively easy to model simple Petri-nets. >The implementation enables simulation of the modelled systems, too, if >the systems are not excessively large. > >If you are interested in this implementation, the source code and >the documentation (in German) are available in tar-unix-format on >a SUN streamer cassette. The syntax of KA-Prolog is very much like that of >C-Prolog, so it should be relatively easy to port the system to C-Prolog >or to a similar dialect of Prolog. Thomas Kropf (kropf@ira.uka.de) writes: (Please note that below we are quoting Thomas Kropf quoting Roger Hale). >The email I got once follows now: >____________________________________________________ > >From: Roger Hale <rwsh%computer-lab.cambridge.ac.uk@NSFNET-RELAY.AC.UK> > >You don't make it clear what you understand a "temporal logic programming >language" to be. So, apologies if you are already aware of the following, >but... > >I am aware of at least four programming languages based on temporal logic. Two >of them, Dov Gabbay's Temporal Prolog and Martin Abadi's Templog, are logic >programming languages in the usual sense (resolution, unification...). The >third, Ben Moszkowski's Tempura, is more like an imperative (deterministic) >parallel programming language which is a subset of temporal logic (programming >language = subset of specification language). The fourth, Masahiro Fujita's >Tokio, is similar to Tempura but permits a degree of non-determinism (using >the backtracking features of prolog). In Tempura and Tokio it is the >variables that are temporal (predicates are static), whereas in Temporal >Prolog and Templog it is the other way round. > >Tempura is described in Moszkowski's book "Executing Temporal Logic Programs" >(pub. Cambridge University Press, 1986) and in my article "Temporal Logic >Programming" in "Temporal Logics and Their Applications" (editor Galton, A., >publisher Academic Press, 1987). A public domain interpreter for Tempura >(written in C) is available from me, preferably by tape but possibly by email. >The interpreter is a research system, but others have managed to make >significant use of it. > >Tokio is described in "Tokio: Logic Programming Language based on Temporal >Logic and Its Compilation to Prolog" by Fujita et al in "Proceedings of the >Third International Conference on Logic Programming" (pub Springer LNCS, >1986). There is a public domain version of Tokio available from Tokyo >University - contact Masahiro Fujita (fujita@p.cs.uiuc.edu) for details. (There seems to be a problem with this. At least our mailer claims that no such user exists in either p.cs.uiuc.edu or cs.uiuc.edu.) Thomas Kropf (kropf@ira.uka.de) continues quoting Roger Hale who continues by saying: >Templog is described by Abadi and Manna in their article "Temporal Logic >Programming" in Proc. IEEE Symposium on Logic Programming, 1987. I don't know >whether there is an implementation of the language. > >Temporal Prolog is described in Gabbay's article "Temporal and Modal Logic >Programming" in the book "Temporal Logics and Their Applications" (see above). >Again, I'm not sure whether there's an implementation available - try >contacting Prof. Gabbay at Dept. of Computing, Imperial College, 180 Queen's >Gate, London SW7 2BZ, England. (Unfortunately no answer from Prof. Gabbay yet.) Thomas Kropf (kropf@ira.uka.de) writes: >The email I got once follows now: >____________________________________________________ >From: "Ed C. Snible" <mailrus!enuxha.eas.asu.edu!snible@bikini.cis.ufl.edu> > >We do a lot of things on temporal logic here and have several languages based >on it. None are currently available via ftp but if you are interested I can >mail you a "Chronolog" compiler I wrote for a class where the assignment was >to implement a temporal logic language. (It's written in Prolog and itself >and it compiles to prolog. Its about 200 lines of Prolog). > >(Chronolog is a "tiny" temporal logic language, an example would be: > > first fib(1). > first next fib(1). > next next fib(Z):- fib(X), next fib(Y), Z is X+Y. >) > >Ed Snible >...!ncar!noao!asuvax!enuxha!snible >snible@enuxha.eas.asu.edu (Unfortunately, we were unable to contact Ed Snible to check any details) 2> temporal logic theorem provers (e.g. resolution methods, tableau methods, > automata theoretic methods, proof editors) Rajeev Gore (Rajeev.Gore@computer-lab.cambridge.ac.uk) writes: >I saw your message in comp.theory about temporal logic tools. I am not >really involved with the implementation of a *serious* temporal logic >theorem prover but my thesis is on Cut-free sequent systems for >temporal logic. Are you doing any theoretical work on temporal logic >theorem proving ? If so, I would appreciate receiving any technical >reports that you have written. Thomas Kropf (kropf@ira.uka.de) writes: > A prover for PTL (propositional temporal logic) has been written by Geert > Janssen. His address is: Geert Janssen <geert@ele.tue.nl>, Eindhoven > University of Technology, The Nederlands Geert Janssen (geert@es.ele.tue.nl) writes: >... yes, I do have a satisfiability checker program for Propositional >Temporal Logic (The Manna/Pnueli logic). And of course I will let you have a >copy of it, i.e. if you will respect the copyright statement as mentioned in >the file COPYRIGHT. Terttu Orci (terttu@cs.umu.se) from the University of Umea, Sweden, has implemented a resolution theorem prover for the modal logic Q. A reference is "Clause Graph Proof Procedure for Model Logic Q" in Proceedings of STEP-90 (the Annual Conference of the Finnish Artificial Intelligence Society). 3> temporal logic model checkers (e.g. for CTL, FCTL, linear time logic and > full branching time logic) Edmund Clarke (Edmund.Clarke@G.GP.CS.CMU.EDU) writes: >We have developed a large number of tools for temporal logic model >checking. Our current model checking program represents state >transition graphs using Binary Decision Diagrams so that we can handle >extremely large graphs with relative ease (more than 10^20 reachable >states--although state count really ceases to be an interesting >measure at this level). One of my students recently used the tool to >find a subtle error in the cache coherency protocol of a large >multiprocessor. The protocol had well over 10^6 states. We have also >developed a number of tools for process equivalence, hiding, >minimization, etc. that we use in conjunction with the model checking >program for compositional reasoning about complex hierarchically >designed systems. > >We distribute the temporal logic tools freely and would be happy to >send you a copy, however we do ask users to sign a license letter. >In fact, we are anxious to find people who are interested in using the >tools and developing them further in collaboration with us. More detailed information on the model checking tools mentioned by Edmund Clarke can be acquired from David Long (long@A.GP.CS.CMU.EDU) and Kenneth McMillan (mcmillan@CHAOS.GP.CS.CMU.EDU). I will not include any details here. A. Arnold (arnold@geocub.greco-prog.fr) writes: >Our Lab has developped a model-checker, named MEC, for alternation-depth-1 >mu-calculus. It is described in >A. Arnold. MEC: a system for constructing and analysing transition systems. >in Automatic Verification of Finite State Systems (ed. J. Sifakis) >Lect. Notes Comput. Sci. 407 (1989) 117-132. > >It runs on Sun stations and can be obtained freely for academic uses only. >Contact D. Begay > Universite Bordeaux I > LaBRI > 351, cours de la Liberation > F-33405 Talence > begay@geocub.gerco-prog.fr Thomas Kropf (kropf@ira.uka.de) writes: > We have also implemented a prover for a subset of PTL at our institute, but > it is tailored to the purpose of hardware verification. 4) general theorem provers which have been instantiated for temporal logic (this category was actually not included in the original posting) Edmund Clarke (Edmund.Clarke@G.GP.CS.CMU.EDU) writes: >My group has also developed a number of parallel algorithms for >symbolic computation and theorem proving. All of the programs >run on 16 processor Encore Multimaxes and the 64 processor RP3 >at IBM Yorktown Heights Research Center: > >1) Parthenon--parallel resolution theorem prover > >2) Parallel Grobner basis algorithm > >3) Parallel program for constructing Ordered Binary Decsion Diagrams. > >We are currently developing a theorem prover (called Analytica) >that runs on top of Mathematica. This seems like a particularly >powerful combination. So far, we have used it to prove a number >of nontrivial theorems in Analysis: > >1) Wierstrass' proof of the existence of a continuous nowhere >differentiable function (3-4 lemmas, each of which is proved >completely automatically) > >2) Uniform approximation of a continuous function by the >sequence of Bernstein Polynomials (Again 3-4 lemmas) > >3) All problems in chapter 2 of Ramanujan's notebooks completely >automatically. > >We should have a version of this to distribute sometime in the >summer. Roger Hale (rwsh@cam.sri.com) writes: >VERIFICATION > >A promising approach to verification (and one you do not mention) is to embed >the temporal logic of your choice in higher-order logic, and use a proof >assistant for higher-order logic to conduct proofs. This technique has been >tried for Mike Gordon's HOL proof asistant (available free from Cambridge >University). Embeddings of classical (Manna & Pnueli) TL and ITL have been >done already. > >This approach has the advantage that you are not limited to (say) a >particular propositional TL; other theories (arithmetic, lists, etc) can >be brought to bear when necessary. The disadvantage (well, maybe...) >is the lack of automation; in principle, any decision procedure can >be coded in ML (the meta-language of HOL), but in practice it will probably >run very slowly. Thomas Kropf (kropf@ira.uka.de) writes: > We ourselves spent some time in defining a full first order temporal logic > in Gordons HOL-System. But since the deduction theorem of "classical" > logic does not hold in general in temproal logic (see e.g. Kroegers > "Temporal Logic of Programs" Springer, p. 28) we stopped this activity. > All tactics and rules of this system would have been to be reimplemented. Tobias Nipkow (Tobias.Nipkow@computer-lab.cambridge.ac.uk) writes: >Although I cannot offer a temporal logic theorem prover, you might be >interested in the generic theorem prover Isabelle. Isabelle can be >parameterized by the description of the syntax and inference rules of some >object logic. We have various instantiations of Isabelle for classical and >constructive, first-order and higher-order logics, and set theories. >Unfortunately, there is no temporal logic instantiation yet, although it >wouldn't require much work to create one (but we haven't got the time). > >If you are interested in finding out more about Isabelle, let me know and I >can send you some references. Isabelle is free and comes with a manual. Rajeev Gore (Rajeev.Gore@computer-lab.cambridge.ac.uk) writes: >Thank you for your message. Please keep me informed of any theoretical >responses to your initial query. There is a strong hardware verification >group here at Cambridge led by Dr. Michael Gordon. They use HOL >(Higher Order Logic) which is a system written in ML (I think). In >particular, one of his students is working on verification of >communication protocols using HOL. I have forwarded your message to >each of them and have included their email addresses below. > >Michael Gordon: mjcg@cl.cam.ac.uk >Rachel Cardell-Oliver: rco@cl.cam.ac.uk Ilkka Niemela (ini@rhea.hut.fi or Ilkka_Niemela@hut.fi) and Heikki Tuominen from the Helsinki University of Technology have implemented a system called HLM (Helsinki Logic Machine) which contains a set of tools for various applications. The emphasis lies in intentional logics and the system contains e.g. theorem provers for more than 60 different logical systems (including several temporal logics, CTL in particular) and model checkers (e.g. for CTL). A reference is Ilkka Niemela and Heikki Tuominen: Helsinki Logic Machine: a System for Logical Expertise. Helsinki University of Technology, Digital Systems Laboratory Technical report B1, Dec 1987, 57p. The system is implemented in Quintus Prolog running on a VMS system and is available free of cost to academic institutions. 5) Replies that do not fall into the previous categories Thomas Kropf (kropf@ira.uka.de) writes: (Please note that we are quoting Thomas Kropf quoting Paul Fishwick quoting Brad Miller.) >The email I got once follows now: >____________________________________________________ > >... you might be interested in TEMPOS, a superset of the >RHET and TIMELOGIC languages developed here. > >You can get a tape (for a symbolics or explorer) for $150. including >documentation, or if you just want doc: > >TR 231 (the TIMELOGIC Reasoning System by Koomen) $1.50 >TR 238 (the RHET User manual by Allen & Miller) $8.75, appendix documents > TEMPOS >TR 239 (The RHET Programmer's manual by Miller) $6.50 > >Send orders to address in header or sig of this meessage, to the attention >of "Peg Meeker". > >The nice thing about TIMELOGIC is it handles time as relations between >intervals rather than as just discrete points. I highly recommend checking >it out! > >More info: > > NAME: Rhet > VERSION: 16.x > SRC/MACHINE/OS: Common Lisp with extensions / Explorer 4.x and > Symbolics 7.x > AVAILABILITY: Full Sources are distributed to anyone, upon signing a > license/disclaimer for non-commercial use. > COST: $150 (academic), TR 238 (user's manual) for $8.75, TR 239 > (programmer's guide [for source hackers]) for $6.50. > Non-academic institutions are requested to send > whatever they can afford over $150 to help defray > expenses. > FEATURES: > This is a Knowledge Representation system based on concepts > proved with HORNE. It includes 2 major modes for representing > knowledge (as Horn Clauses or as frames), which are interchangable; > a type subsystem for typed and type restricted objects (including > variables); E-unification; negation; forward and backward chaining; > complete proofs (prove, disprove, find the KB inconsistent, or > claim a goal is neither provable nor disprovable); incremental > compilation (future); contextual reasoning; truth maintenance; > intelligent backtracking; full LISP compatibility (can call or > be called by lisp); upward compatible with HORNE; Allen & Koomen's > TEMPOS time interval reasoning subsystem; frames have KL-1 type > features, plus arbitrary predicate restrictions on slots within a frame > as well as default values for slots; separate subsystem providing > advanced user-interface facilities and ZMACS interface on the > lispms. > CONTACT: > Admin: (distribution and TRs) Peg Meeker (peg@cs.rochester.edu) > Technical: Brad Miller (miller@cs.rochester.edu) > James Allen (james@cs.rochester.edu) > > Computer Science Department > University of Rochester > Rochester, NY 14627 > NOTES: > This software is still under active development. Tape includes TEMPOS > interface to TIMELOGIC system (TR 231 $1.50), and RPRS Plan recognition > system (implemented in Rhet). Mailing list for bugs and/or developments. > DATED: June 1989 Up-to-date information is available from peg@cs.rochester.edu. She kindly informed us of the fact that the software is also available without charge by anonymous ftp from CS.ROCHESTER.EDU:/pub/knowledge-tools/*. Thomas Kropf (kropf@ira.uka.de) writes: >The email I got once follows now: >____________________________________________________ > >From: munnari!extro.ucc.su.OZ.AU!marwan@uunet.UU.NET > (Marwan Jabri, Sydney Univ. Elec. Eng., Tel: +61-2-692 2240) >I have done some work on temporal logic for formal hardware verification >and we have a system called TEMPO which is written in PROLOG. I can >give you the prolog code but you will need Quintus Prolog or a like to >run it. (Please note again that we are quoting Thomas Kropf quoting Marwan Jabri.) Thank you very much for all the replies! Roope Kaivola University of Helsinki rkaivola@cc.helsinki.fi Department of Computer Science tel. +358-0-708 4163 Teollisuuskatu 23 SF-00510 Helsinki Finland