The complementation problem for Büchi automata with applications to temporal logic

2005 ◽  
pp. 465-474 ◽  
Author(s):  
A. Prasad Sistla ◽  
Moshe Y. Vardi ◽  
Pierre Wolper
Keyword(s):  
Temporal Logic ◽  
Büchi Automata ◽  
Buchi Automata

Tool support for learning Büchi automata and linear temporal logic

2008 ◽  
Vol 21 (3) ◽  
pp. 259-275 ◽  
Author(s):  
Yih-Kuen Tsay ◽  
Yu-Fang Chen ◽  
Ming-Hsien Tsai ◽  
Kang-Nien Wu ◽  
Wen-Chin Chan ◽  
...  
Keyword(s):  
Temporal Logic ◽  
Linear Temporal Logic ◽  
Tool Support ◽  
Büchi Automata ◽  
Buchi Automata

Conversion Algorithm of Linear-Time Temporal Logic to Buchi Automata

2014 ◽  
Vol 9 (4) ◽  
Author(s):  
Laixiang Shan ◽  
Zheng Qin ◽  
Shengnan Li ◽  
Renwei Zhang ◽  
Xiao Yang
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Conversion Algorithm ◽  
Büchi Automata ◽  
Linear Time Temporal Logic ◽  
Buchi Automata

scholarly journals The complementation problem for Büchi automata with applications to temporal logic

1987 ◽  
Vol 49 (2-3) ◽  
pp. 217-237 ◽  
Author(s):  
A. Prasad Sistla ◽  
Moshe Y. Vardi ◽  
Pierre Wolper
Keyword(s):  
Temporal Logic ◽  
Büchi Automata ◽  
Buchi Automata

scholarly journals Synthesizing Good-Enough Strategies for LTLf Specifications

2021 ◽  
Author(s):  
Yong Li ◽  
Andrea Turrini ◽  
Moshe Y. Vardi ◽  
Lijun Zhang
Keyword(s):  
Temporal Logic ◽  
Linear Temporal Logic ◽  
Synthesis Algorithm ◽  
Infinite Words ◽  
Büchi Automata ◽  
Winning Strategies ◽  
Deterministic Automata ◽  
Computationally Expensive ◽  
Buchi Automata

We consider the problem of synthesizing good-enough (GE)-strategies for linear temporal logic (LTL) over finite traces or LTLf for short. The problem of synthesizing GE-strategies for an LTL formula φ over infinite traces reduces to the problem of synthesizing winning strategies for the formula (∃Oφ)⇒φ where O is the set of propositions controlled by the system. We first prove that this reduction does not work for LTLf formulas. Then we show how to synthesize GE-strategies for LTLf formulas via the Good-Enough (GE)-synthesis of LTL formulas. Unfortunately, this requires to construct deterministic parity automata on infinite words, which is computationally expensive. We then show how to synthesize GE-strategies for LTLf formulas by a reduction to solving games played on deterministic Büchi automata, based on an easier construction of deterministic automata on finite words. We show empirically that our specialized synthesis algorithm for GE-strategies outperforms the algorithms going through GE-synthesis of LTL formulas by orders of magnitude.

scholarly journals UNITY and Büchi automata

2021 ◽  
Vol 33 (2) ◽  
pp. 185-205 ◽  
Author(s):  
Wim H. Hesselink
Keyword(s):  
Temporal Logic ◽  
Linear Temporal Logic ◽  
Concurrent Program ◽  
Büchi Automata ◽  
Buchi Automata ◽  
Classical Construction

AbstractUNITY is a model for concurrent specifications with a complete logic for proving progress properties of the form “P leads to Q”. UNITY is generalized to U-specifications by giving more freedom to specify the steps that are to be taken infinitely often. In particular, these steps can correspond to non-total relations. The generalization keeps the logic sound and complete. The paper exploits the generalization in two ways. Firstly, the logic remains sound when the specification is extended with hypotheses of the form “F leads to G”. As the paper shows, this can make the logic incomplete. The generalization is used to show that the logic remains complete, if the added hypotheses “F leads to G” satisfy “F unless G”. The main result extends the applicability and completeness of UNITY logic to proofs that a given concurrent program satisfies any given formula of LTL, linear temporal logic, without the next-operator which is omitted because it is sensitive to stuttering. For this purpose, the program, written as a UNITY program, is extended with a number of boolean variables. The proof method relies on implementing the LTL formula, i.e., restricting the specification in such a way that only those runs remain that satisfy the formula. This result is a variation of the classical construction of a Büchi automatonfor a given LTL formula that accepts precisely those runs that satisfy the formula.

Limit-Deterministic Büchi Automata for Linear Temporal Logic

2016 ◽  
pp. 312-332 ◽  
Author(s):  
Salomon Sickert ◽  
Javier Esparza ◽  
Stefan Jaax ◽  
Jan Křetínský
Keyword(s):  
Temporal Logic ◽  
Linear Temporal Logic ◽  
Büchi Automata ◽  
Buchi Automata

Almost linear Büchi automata

2012 ◽  
Vol 22 (2) ◽  
pp. 203-235 ◽  
Author(s):  
TOMÁŠ BABIAK ◽  
VOJTĚCH ŘEHÁK ◽  
JAN STREJČEK
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Linear Temporal Logic ◽  
Practical Relevance ◽  
New Class ◽  
Büchi Automata ◽  
Buchi Automata ◽  
Alternating Automata

We introduce a new fragment of linear temporal logic (LTL) called LIO and a new class of Büchi automata (BA) called almost linear Büchi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. As we expect there to be applications of our results in model checking, we use two standard sources of specification formulae, namely Spec Patterns and BEEM, to study the practical relevance of the LIO fragment, and to compare our translation of LIO to ALBA with two standard translations of LTL to BA using alternating automata. Finally, we demonstrate that the LIO to ALBA translation can be much faster than the standard translation, and the resulting automata can be substantially smaller.

Sign in / Sign up

Export Citation Format

Share Document