Temporal Logics Zoo
Motivation and Objectives:
The present wiki space is inspired by the complexity zoo counterpart (https://complexityzoo.uwaterloo.ca/Complexity_Zoo) and is an effort to bring together specification languages, tools, and resources employed in robotics and control. The main goals of the wiki space are:
- to build a repository of the main specification languages employed in robotics and control
- to present the relationships between them with respect to syntax and semantics in order to clarify and help with the choice of appropriate TL for specific applications
- to build a repository of tutorials, use cases, tools, and standard benchmark data and missions
- to engage the community to maintain a dynamic and curated reference resource for TL in robotics and control
- to survey the needs and accomplishments of the field through shared media
- to periodically publish a report on progress, current problems, and long-term direction of the field
Format
In order to provide a useful resource for researchers, we employ a "less is better" principle in the sense that descriptions are should be as concise as possible outlining the most relevant knowledge. The pages in this space are curated and must follow proper citation conventions. However, references should be as much as possible to externally hosted repositories such as IEEEXplore, Scopus, etc. Again, the goal is not to have an exhaustive list of papers and tools, but to provide a dynamic community-curated reference for starting or seasoned researchers in robotics and control that employ temporal logics.
Quick overview of Temporal Logics
| Temporal Logic | Year | Resources | Benchmark problems | Tools List | Reference |
|---|---|---|---|---|---|
| LTL | 1977 | The Rise and Fall of LTL (Moshe Vardi): https://www.cs.rice.edu/~vardi/papers/gandalf11-myv.pdf | ltl2ba: http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ ltl2dra: http://www.ltl2dstar.de/ | A. Pnueli, The temporal logic of programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), 1977, 46–57. doi:10.1109/SFCS.1977.32 | |
| scLTL | |||||
| STL | 2004 | On Signal Temporal Logic (Alez Donze): https://people.eecs.berkeley.edu/~sseshia/fmee/lectures/EECS294-98_Spring2014_STL_Lecture.pdf | Breach: https://people.eecs.berkeley.edu/~donze/breach_page.html BluSTL: https://github.com/BluSTL/BluSTL | O. Maler and D. Nickovic. Monitoring temporal properties of continuous signals. In FORMATS/FTRTFT, pages 152–166, 2004. | |
| MTL | 1990 | Decision Problems for Metric Temporal Logic (Joel Ouaknine): https://www.itu.dk/qmc2012/joelouaknine4.pdf | S-TaLiRo: https://sites.google.com/a/asu.edu/s-taliro/s-taliro | R. Koymans. Specifying real-time properties with metric temporal logic. Real-Time Syst., 2(4):255–299, 1990. | |
| BLTL | |||||
| GR(1) | 2006 | Tutorial on Synthesis (Bernd Finkbeiner): https://www.react.uni-saarland.de/teaching/games-synthesis-robotics-11/tutorial.pdf | slugs: https://github.com/VerifiableRobotics/slugs TuLiP: https://github.com/tulip-control/tulip-control LTLMoP: https://ltlmop.github.io/ | N. Piterman, A. Pnueli, Y. Saʼar. Synthesis of reactive(1) designs. Proc. of the 7th Int. Conf. on Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Comput. Sci., vol. 3855, , Springer-Verlag (2006), pp. 364–380 | |
| MITL | |||||
| PrSTL | 2016 | CrSPrSTL: https://github.com/dsadigh/CrSPrSTL | D. Sadigh, A. Kapoor. Safe Control under Uncertainty with Probabilistic Signal Temporal Logic. Robotics: Science and Systems 2016. | ||
| C2TL | 2016 | S. Jha, V. Raman: Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty. NFM 2016: 117-132. | |||
| CTL | 1981 | Lecture slides (Alessandro Artale): http://www.inf.unibz.it/~artale/FM/slide4.pdf | E.M. Clarke, E.A. Emerson. Design and synthesis of synchronisation skeletons using branching time temporal logic. Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science, vol. 131. Springer (1981), Berlin: 52–71. | ||
| SpaTeL | 2015 | http://sites.bu.edu/hyness/files/2014/10/SpaTeL.rar | I. Haghighi, A. Jones, Z. Kong, E. Bartocci, R. Grosu and C. Belta, SpaTeL: A Novel Spatial-Temporal Logic and Its Applications to Networked Systems, Hybrid Systems: Computation and Control (HSCC) 2015. | ||
| TWTL | 2014 | PyTWTL: http://hyness.bu.edu/twtl/ | C.-I. Vasile, D. Aksaray, and C. Belta. "Time Window Temporal Logic." arXiv preprint, arXiv:1602.04294, 2016. | ||
\mu-calculus | 1983 | D. Kozen. Results on the Propositional μ-Calculus. Theoretical Computer Science. 27 (3): 333–354. | |||
| process algebra |
To help you on your way, we've inserted some of our favourite macros on this home page. As you start creating pages, blogging and commenting you'll see the macros below fill up with all the activity in your space.