Document Open Access Logo

Past, Present, and Infinite Future

Author Thomas Wilke

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2016.95.pdf
  • Filesize: 449 kB
  • 14 pages

Document Identifiers

Author Details

Thomas Wilke

Cite As Get BibTex

Thomas Wilke. Past, Present, and Infinite Future. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 95:1-95:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ICALP.2016.95

Abstract

I was supposed to deliver one of the speeches at Wolfgang Thomas's retirement ceremony. Wolfgang had called me on the phone earlier and posed some questions about temporal logic, but I hadn't had good answers at the time. What I decided to do at the ceremony was to take up the conversation again and show how it could have evolved if only I had put more effort into answering his questions. Here is the imaginary conversation with Wolfgang.

The contributions are (1) the first direct translation from counter-free omega-automata into future temporal formulas, (2) a definition of bimachines for omega-words, (3) a translation from arbitrary temporal formulas (including both, future and past operators) into counter-free omega-bimachines, and (4) an automata-based proof of separation: every arbitrary temporal formula is equivalent to a boolean combination of pure future, present, and pure past formulas when interpreted in omega-words.

Subject Classification

Keywords
  • linear-time temporal logic
  • separation
  • backward deterministic omega-automata
  • counter freeness

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Olivier Carton. Personal communication. Google Scholar
  2. Olivier Carton. Right-sequential functions on infinite words. In Farid M. Ablayev and Ernst W. Mayr, editors, Computer Science - Theory and Applications, 5th International Computer Science Symposium in Russia, CSR 2010, Kazan, Russia, June 16-20, 2010. Proceedings, volume 6072 of Lecture Notes in Computer Science, pages 96-106. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-13182-0_9.
  3. Olivier Carton and Max Michel. Unambiguous Büchi automata. In Gaston H. Gonnet, Daniel Panario, and Alfredo Viola, editors, LATIN 2000: Theoretical Informatics, 4th Latin American Symposium, Punta del Este, Uruguay, April 10-14, 2000, Proceedings, volume 1776 of Lecture Notes in Computer Science, pages 407-416. Springer, 2000. URL: http://dx.doi.org/10.1007/10719839_40.
  4. Volker Diekert and Paul Gastin. First-order definable languages. In Jörg Flum, Erich Grädel, and Thomas Wilke, editors, Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], volume 2 of Texts in Logic and Games, pages 261-306. Amsterdam University Press, 2008. Google Scholar
  5. Calvin C. Elgot and Jorge E. Mezei. On relations defined by generalized finite automata. IBM Journal of Research and Development, 9(1):47-68, Jan 1965. URL: http://dx.doi.org/10.1147/rd.91.0047.
  6. Dov M. Gabbay. The declarative past and imperative future: Executable temporal logic for interactive systems. In Behnam Banieqbal, Howard Barringer, and Amir Pnueli, editors, Temporal Logic in Specification, Altrincham, UK, April 8-10, 1987, Proceedings, volume 398 of Lecture Notes in Computer Science, pages 409-448. Springer, 1987. Google Scholar
  7. Dov M. Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi. On the temporal basis of fairness. In Paul W. Abrahams, Richard J. Lipton, and Stephen R. Bourne, editors, Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada, USA, January 1980, pages 163-173. ACM Press, 1980. URL: http://dl.acm.org/citation.cfm?id=567446, URL: http://dx.doi.org/10.1145/567446.567462.
  8. Johan Anthony Willem Kamp. Tense logic and the theory of linear order. PhD thesis, University of California, Los Angeles, 1968. Google Scholar
  9. Richard E. Ladner. Application of model theoretic games to discrete linear orders and finite automata. Information and Control, 33(4):281-303, 1977. URL: http://dx.doi.org/10.1016/S0019-9958(77)90443-0.
  10. Robert McNaughton and Seymour Papert. Counter-free automata. M.I.T. Press research monographs. M.I.T. Press, 1971. Google Scholar
  11. Dominique Perrin and Jean-Éric Pin. Infinite Words: Automata, Semigroups, Logic, and Games, volume 141 of Pure and Applied Mathematics. Elsevier, Amsterdam, 2004. Google Scholar
  12. Marcel Paul Schützenberger. A remark on finite transducers. Information and Control, 4(2-3):185-196, 1961. URL: http://dx.doi.org/10.1016/S0019-9958(61)80006-5.
  13. Marcel Paul Schützenberger. On finite monoids having only trivial subgroups. Information and Control, 8(2):190-194, 1965. URL: http://dx.doi.org/10.1016/S0019-9958(65)90108-7.
  14. Michael Sipser. Introduction to the Theory of Computation. Cengage Learning, Boston, Mass., 3rd edition, 2013. Google Scholar
  15. Wolfgang Thomas. Star-free regular sets of omega-sequences. Information and Control, 42(2):148-156, 1979. URL: http://dx.doi.org/10.1016/S0019-9958(79)90629-6.
  16. Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Inf. Comput., 115(1):1-37, 1994. URL: http://dx.doi.org/10.1006/inco.1994.1092.
  17. Thomas Wilke. Classifying discrete temporal properties. In Christoph Meinel and Sophie Tison, editors, STACS 99, 16th Annual Symposium on Theoretical Aspects of Computer Science, Trier, Germany, March 4-6, 1999, Proceedings, volume 1563 of Lecture Notes in Computer Science, pages 32-46. Springer, 1999. URL: http://dx.doi.org/10.1007/3-540-49116-3_3.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact