scholarly journals A Framework for Verified Depth-First Algorithms

10.29007/8hkx ◽  
2018 ◽  
Author(s):  
René Neumann
Keyword(s):  
Model Checking ◽  
Programming Languages ◽  
Depth First Search ◽  
Standard Ml ◽  
Executable Code ◽  
Büchi Automata ◽  
Emptiness Problem ◽  
Buchi Automata

We present a framework in Isabelle/HOL for formalizing variants ofdepth-first search. This framework allows to easily prove non-trivialproperties of these variants. Moreover, verified code in severalprogramming languages including Haskell, Scala and Standard ML can begenerated.In this paper, we present an abstract formalization of depth-first search anddemonstrate how it is refined to an efficiently executable version. Further we use the emptiness-problem of Büchi-automata known from model checking as the motivation to present three Nested DFS algorithms. They are formalized, verified and transformed into executable code using our framework.

Synthesis with Mandatory Stop Actions

2021 ◽  
Author(s):  
Giuseppe De Giacomo ◽  
Antonio Di Stasio ◽  
Giuseppe Perelli ◽  
Shufang Zhu
Keyword(s):  
Model Checking ◽  
Finite State Automata ◽  
Deep Impact ◽  
Synthesis Technique ◽  
Büchi Automata ◽  
Finite State ◽  
Ltl Synthesis ◽  
Buchi Automata ◽  
The Impact

We study the impact of the need for the agent to obligatorily instruct the action stop in her strategies. More specifically we consider synthesis (i.e., planning) for LTLf goals under LTL environment specifications in the case the agent must mandatorily stop at a certain point. We show that this obligation makes it impossible to exploit the liveness part of the LTL environment specifications to achieve her goal, effectively reducing the environment specifications to their safety part only. This has a deep impact on the efficiency of solving the synthesis, which can sidestep handling Buchi determinization associated to LTL synthesis, in favor of finite-state automata manipulation as in LTLf synthesis. Next, we add to the agent goal, expressed in LTLf, a safety goal, expressed in LTL. Safety goals must hold forever, even when the agent stops, since the environment can still continue its evolution. Hence the agent, before stopping, must ensure that her safety goal will be maintained even after she stops. To do synthesis in this case, we devise an effective approach that mixes a synthesis technique based on finite-state automata (as in the case of LTLf goals) and model-checking of nondeterministic Buchi automata. In this way, again, we sidestep Buchi automata determinization, hence getting a synthesis technique that is intrinsically simpler than standard LTL synthesis.

Bounded Model Checking for Weak Alternating Büchi Automata

2006 ◽  
pp. 95-108 ◽  
Author(s):  
Keijo Heljanko ◽  
Tommi Junttila ◽  
Misa Keinänen ◽  
Martin Lange ◽  
Timo Latvala
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Büchi Automata ◽  
Buchi Automata

scholarly journals From LTL to unambiguous Büchi automata via disambiguation of alternating automata

2021 ◽  
Author(s):  
Simon Jantsch ◽  
David Müller ◽  
Christel Baier ◽  
Joachim Klein
Keyword(s):  
Model Checking ◽  
Markov Chains ◽  
Important Application ◽  
High Complexity ◽  
The Core ◽  
Büchi Automata ◽  
Deterministic Automata ◽  
Tool Set ◽  
Buchi Automata ◽  
Alternating Automata

AbstractDue to the high complexity of translating linear temporal logic (LTL) to deterministic automata, several forms of “restricted” nondeterminism have been considered with the aim of maintaining some of the benefits of deterministic automata, while at the same time allowing more efficient translations from LTL. One of them is the notion of unambiguity. This paper proposes a new algorithm for the generation of unambiguous Büchi automata (UBA) from LTL formulas. Unlike other approaches it is based on a known translation from very weak alternating automata (VWAA) to NBA. A notion of unambiguity for alternating automata is introduced and it is shown that the VWAA-to-NBA translation preserves unambiguity. Checking unambiguity of VWAA is determined to be PSPACE-complete, both for the explicit and symbolic encodings of alternating automata. The core of the LTL-to-UBA translation is an iterative disambiguation procedure for VWAA. Several heuristics are introduced for different stages of the procedure. We report on an implementation of our approach in the tool and compare it to an existing LTL-to-UBA implementation in the tool set. Our experiments cover model checking of Markov chains, which is an important application of UBA.

A Sweep-Line Method for Büchi Automata-based Model Checking

2014 ◽  
Vol 131 (1) ◽  
pp. 27-53 ◽  
Author(s):  
Sami Evangelista ◽  
Lars Michael Kristensen
Keyword(s):  
Model Checking ◽  
Line Method ◽  
Büchi Automata ◽  
Buchi Automata ◽  
Sweep Line
Sign in / Sign up

Export Citation Format

Share Document