https://scholars.lib.ntu.edu.tw/handle/123456789/607928
DC Field | Value | Language |
---|---|---|
dc.contributor.author | YIH-KUEN TSAY | en_US |
dc.contributor.author | Vardi M.Y. | en_US |
dc.creator | Tsay Y.-K;Vardi M.Y. | - |
dc.date.accessioned | 2022-04-26T06:17:31Z | - |
dc.date.available | 2022-04-26T06:17:31Z | - |
dc.date.issued | 2021 | - |
dc.identifier.issn | 03029743 | - |
dc.identifier.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 | - |
dc.identifier.uri | https://scholars.lib.ntu.edu.tw/handle/123456789/607928 | - |
dc.description.abstract | 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. | - |
dc.relation.ispartof | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | - |
dc.subject | Alternating automata | - |
dc.subject | Automata | - |
dc.subject | Automata-theoretic approach | - |
dc.subject | B?chi automata | - |
dc.subject | Linear temporal logic | - |
dc.subject | LTL | - |
dc.subject | PTL | - |
dc.subject | Translation | - |
dc.subject | Two-way automata | - |
dc.subject | Very weak automata | - |
dc.subject | Computer circuits | - |
dc.subject | Model checking | - |
dc.subject | Temporal logic | - |
dc.subject | Automaton | - |
dc.subject | Buchi automata | - |
dc.subject | Very weak automaton | - |
dc.subject | Automata theory | - |
dc.title | From Linear Temporal Logics to Büchi Automata: The Early and Simple Principle | en_US |
dc.type | book chapter | en |
dc.identifier.doi | 10.1007/978-3-030-91384-7_2 | - |
dc.identifier.scopus | 2-s2.0-85120904968 | - |
dc.relation.pages | 8-40 | - |
dc.relation.journalvolume | 13030 LNCS | - |
item.openairetype | book chapter | - |
item.openairecristype | http://purl.org/coar/resource_type/c_18cf | - |
item.fulltext | no fulltext | - |
item.grantfulltext | none | - |
item.cerifentitytype | Publications | - |
crisitem.author.dept | Information Management | - |
crisitem.author.orcid | 0000-0002-5960-1615 | - |
crisitem.author.parentorg | College of Management | - |
Appears in Collections: | 資訊管理學系 |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.