Zobrazeno 1 - 10
of 21
pro vyhledávání: '"Salomon Sickert"'
Autor:
David Müller, Salomon Sickert
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 256, Iss Proc. GandALF 2017, Pp 180-194 (2017)
We introduce a new translation from linear temporal logic (LTL) to deterministic Emerson-Lei automata, which are omega-automata with a Muller acceptance condition symbolically expressed as a Boolean formula. The richer acceptance condition structure
Externí odkaz:
https://doaj.org/article/0babda1fc870438fbe2c82a9985e6f2f
Publikováno v:
Journal of the ACM
We present a unified translation of linear temporal logic (LTL) formulas into deterministic Rabin automata (DRA), limit-deterministic Büchi automata (LDBA), and nondeterministic Büchi automata (NBA). The translations yield automata of asymptoticall
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b389753ace8acde3b17fee4e44eaed61
https://doi.org/10.1145/3417995
https://doi.org/10.1145/3417995
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030992521
FOSSACS
FOSSACS, Apr 2022, Munich, Germany. pp.140-160, ⟨10.1007/978-3-030-99253-8_8⟩
FOSSACS
FOSSACS, Apr 2022, Munich, Germany. pp.140-160, ⟨10.1007/978-3-030-99253-8_8⟩
While the complexity of translating future linear temporal logic (LTL) into automata on infinite words is well-understood, the size increase involved in turning automata back to LTL is not. In particular, there is no known elementary bound on the com
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7de9f6b51e6206acede12952a7706c67
http://arxiv.org/abs/2201.10267
http://arxiv.org/abs/2201.10267
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030995263
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Tools and Algorithms for the Construction and Analysis of Systems
In 2021, Casares, Colcombet, and Fijalkow introduced the Alternating Cycle Decomposition (ACD) to study properties and transformations of Muller automata. We present the first practical implementation of the ACD in two different tools, Owl and Spot,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6970dd4ce9470c58633518b64fa8db2c
https://doi.org/10.1007/978-3-030-99527-0_6
https://doi.org/10.1007/978-3-030-99527-0_6
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783031223365
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Principles of Systems Design
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Principles of Systems Design
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::96bcb876a7ade2a16bfdba1b9f6c5ca6
https://doi.org/10.1007/978-3-031-22337-2_10
https://doi.org/10.1007/978-3-031-22337-2_10
The automation of decision procedures makes certification essential. We suggest to use determinacy of turn-based two-player games with regular winning conditions in order to generate certificates for the number of states that a deterministic finite a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::dae02451e83df65c4025beb30353b95c
http://arxiv.org/abs/2107.01566
http://arxiv.org/abs/2107.01566
Publikováno v:
Acta Informatica. 57:3-36
The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e6b625dba2d9268e6ede5f084c8ef3fe
https://doi.org/10.1007/s00236-019-00349-3
https://doi.org/10.1007/s00236-019-00349-3
Publikováno v:
Automated Technology for Verification and Analysis ISBN: 9783030888848
ATVA
ATVA
The automation of decision procedures makes certification essential. We suggest to use determinacy of turn-based two-player games with regular winning conditions in order to generate certificates for the number of states that a deterministic finite a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::55c3aa82ea6cf4ec3fcc20b1c73225d8
https://doi.org/10.1007/978-3-030-88885-5_4
https://doi.org/10.1007/978-3-030-88885-5_4
Publikováno v:
Formal Methods in System Design. 49:219-271
We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula $$\varphi $$ź. The automaton is the product of a co-Buchi automaton for $$\varphi $$ź and an array of Rabin automata, one for each $${\mathbf {
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9a0db40e0d8d7953e91a9f88bebedb03
https://doi.org/10.1007/s10703-016-0259-2
https://doi.org/10.1007/s10703-016-0259-2
Publikováno v:
LICS
We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic B\"uchi automata, and nondeterministic B\"uchi automata. The translations yield automata of asymptotically optimal size (double or single exponent
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::be3847c940d5502f62a94c48d6e176fe
http://arxiv.org/abs/1805.00748
http://arxiv.org/abs/1805.00748