https://scholars.lib.ntu.edu.tw/handle/123456789/607928
標題: | From Linear Temporal Logics to Büchi Automata: The Early and Simple Principle | 作者: | YIH-KUEN TSAY Vardi M.Y. |
關鍵字: | Alternating automata;Automata;Automata-theoretic approach;B?chi automata;Linear temporal logic;LTL;PTL;Translation;Two-way automata;Very weak automata;Computer circuits;Model checking;Temporal logic;Automaton;Buchi automata;Very weak automaton;Automata theory | 公開日期: | 2021 | 卷: | 13030 LNCS | 起(迄)頁: | 8-40 | 來源出版物: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | 摘要: | The automata-theoretic approach advocates reducing problems in an application domain to those in automata theory. When there are multiple paths for the reduction, leaving the realm of application and entering that of automata as early as possible should be preferred, to take full advantages of the abundant algorithmic techniques from the latter. This makes the entire reduction simpler for intuitive understanding and easier for correctness proofs. Indeed, for linear-time temporal logic model checking, there are quite a few ways for translating a temporal formula into an equivalent B?chi automaton. They all go through one or more types of automata as intermediaries, with various interspersing formula manipulation and automaton generation along the way. Among them, translations via alternating automata apparently better adhere to the aforementioned “early and simple” principle. When it comes to translating temporal formulae with past operators, algorithms following the principle generalize more easily by using a two-way alternating automaton as the first intermediary. In this paper, we give a tutorial presentation of two translation algorithms adhering to the early and simple principle, one for formulae with only future operators and the other for formulae with both future and past operators. They are adaptations of existing works, with a substantially different exposition, further improving simplicity for understanding and easiness for proofs. In particular, we have tried wherever possible to avoid using types of automata or notations that are less common. The relevant notion of a very weak automaton is introduced with two equivalent defining conditions, each offering its unique advantage in a suitable context. Finally, we discuss the role of minimization in such an approach to translation of temporal formulae. ? 2021, Springer Nature Switzerland AG. |
URI: | https://www.scopus.com/inward/record.uri?eid=2-s2.0-85120904968&doi=10.1007%2f978-3-030-91384-7_2&partnerID=40&md5=a33196b3509afecb4abbade115e52e1f https://scholars.lib.ntu.edu.tw/handle/123456789/607928 |
ISSN: | 03029743 | DOI: | 10.1007/978-3-030-91384-7_2 |
顯示於: | 資訊管理學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。