Unusual Effectiveness of Automata in Logic: Threads and Synthesis
Delve into the intriguing journey of automata in logic, from Hilbert's program to modern applications. Explore the fusion of modal and temporal logic with computer science, unlocking new possibilities. Discover key players, pivotal moments, and the intricate web of collaboration that shaped this fascinating field.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
On the Unusual Effectiveness of Automata in Logic Pierre Wolper University of Li ge 1
Back to Haifa after 40 Years 2
What this talk is about A question: How come am I here today giving this talk ? Answer: A story weaved from many threads o The science that led to the work I did with Moshe o The development of an unusually effective collaboration o The details and coincidences that are necessary for a good story 3
The initial threads Hilbert s program and the decidability of logics o Progress: Moj esz Presburger (Warsaw, 1904 1943) , ber der Vollst ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen (1929) o Limits: Kurt G del 1931, Alan Turing 1936, Alonzo Church 1936 Finite Automata and language theory o Equivalence of formalisms (DFA, NFA and regular languages): Kleene, Representation of Events in Nerve Nets and Finite Automata, 1951 o Algorithms for finite automata: Michael Rabin and Dana Scott, Finite Automata and Their Decision Problems, 1959. 4
A first merge : using finite automata to decide logics J. Richard B chi o A logic for automata and another view of Presburger arithmetic decidability: Weak second-order arithmetic and finite automata, 1960 o A stronger logic and automata: On a decision method in restricted second- order arithmetic, 1962 Michael 0. Rabin o SnS and automata on infinite trees: Decidability of second-order theories and automata on infinite trees 5
The modal and temporal logic thread Modal Logic o An early starting point : Clarence Irving Lewis , Implication and the Algebra of Logic, 1912 o Possible world semantics : Saul A. Kripke, A Completeness Theorem in Modal Logic, 1959 Temporal logic o Temporal Logic, semantics, linear and branching : Arthur N. Prior, Time and Modality, 1957 ; Past, Present and Future, 1967 6
Modal Logics Meet Computer Science Temporal logic o A foundational paper: Amir Pnueli, The Temporal Logic of Programs, FOCS, 1977 o Synthesis work: Logic of Programs, Yorktown Heights, May 4 6, 1981 Edmund M. Clarke, E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic Zohar Manna, Pierre Wolper, Synthesis of communicating processes from Temporal Logic specifications Dynamic Logic o In a first-order framework: Vaughan R. Pratt, Semantical considerations on Floyd-Hoare logic, FOCS, 1976 o Propositional and decidability: Michael Fischer & Ladner, Propositional dynamic logic of regular programs, STOC, 1977, JCSS, 1979 V.R. Pratt, A Practical Decision Method for Propositional Dynamic Logic, FOCS 1978 7
Dynamic logic is combined with temporal logic: Process Logic Extend dynamic logic to reason about ongoing behavior o V.R. Pratt, A Practical Decision Method for Propositional Dynamic Logic, STOC 1978 o R. Parikh, A Decidability Result for a Second Order Process Logic, FOCS 1978. o Harel, D. Kozen, R. Parikh, Process Logic: Expressiveness, Decidability, Completeness, FOCS 1980 o H. Nishimura, Descriptively Complete Process Logic, Acta Informatica, 14 (1980) 8
How our Collaboration Started 1978: I arrive at Stanford as a PhD student in CS and start working with Zohar Manna 1981: Moshe Vardi comes to Stanford as a post-doc to work on database theory FOCS, Nashville, TN, October 1981 o Moshe Vardi, Global Decision Problems for Relational Databases o Pierre Wolper, Temporal Logic Can Be More Expressive 9
A First Joint Paper: YAPL Combine Extended Temporal Logic with Dynamic logic with a looping operator Moshe Vardi, Pierre Wolper, Yet Another Process Logic, Logics of Programs, Pittsburgh, PA, June 6-8, 1983 oA meaningful extension odecision procedure (4 exponentials) oEver used ? o108 citations 10
Wrapping up Extended Temporal Logics First report: P. Wolper, M. Y. Vardi, A. P. Sistla, Reasoning about Infinite Computation Paths, FOCS 1983 o Different types of automata as operators : finite prefix, looping, repeating acceptance, alternating. o Decision procedure by constructing an automaton and deciding non emptiness. Final papers: o A. Prasad Sistla, Moshe Y. Vardi, Pierre Wolper: The Complementation Problem for B chi Automata with Applications to Temporal Logic, ICALP 1985, TCS 1987 o Moshe Y. Vardi, Pierre Wolper, Reasoning About Infinite Computations, Information and computation, 1994. 11
Automata-Theoretic (and Probabilistic) Exploiting automata and looking at fair and probabilistic programs Moshe Y. Vardi, Pierre Wolper, Automata Theoretic Techniques for Modal Logics of Programs STOC 1984, JCSS 1986 Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper, Reasoning about Fair Concurrent Programs, STOC 1986 Moshe Y. Vardi, Pierre Wolper, An Automata-Theoretic Approach to Automatic Program Verification (preliminary report), LICS 1986 12
Getting practical (somewhat) Convincing that the automata-theoretic approach to model checking is practical Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper, Mihalis Yannakakis, Memory Efficient Algorithms for the Verification of Temporal Properties, CAV 1990, FMSD 1992. Rob Gerth, Doron A. Peled, Moshe Y. Vardi, Pierre Wolper: Simple on-the-fly automatic verification of linear temporal logic, PSTV 1995 13
Meeting Orna and the branching thread The automata-theoretic approach is efficiently applied to CTL Orna Bernholtz-Kuperman, Moshe Y. Vardi, Pierre Wolper, An Automata-Theoretic Approach to Branching-Time Model Checking, CAV 1994, J. ACM 2000 Orna Kupferman, Moshe Y. Vardi, Pierre Wolper, Module Checking, Inf. Comp. 2001 14
An unusually effective collaboration Only 10 papers, 13 including conference versions of later journal papers. Around 8.400 citations to these papers The secret ? o Combining ideas from various threads of research o Simplicity and clarity let you go further o So does being motivated by the desire to understand o Turning research into an interesting story helps to make it known o Keeping an eye on applications 15
An inspiration for further work Finite automata for dealing with Presburger arithmetic and its extension to integers and reals Computing reachable states of pushdown systems Iterating automata-represented transducers Representing buffer contents by automata in models of weak memory models 16
Fun Parts and a Conclusion Sharing awards oKurt G del Prize 200O oACM Kanellakis Theory and Practice award 2005 oLICS Test of Time award 2006 Visits o Houston 2015 o Li ge 2017 Honoris Causa Doctorate awarded to Moshe A nice thing about being old is that your have old friends Moshe Vardi 17
