scholarly journals A Framework for Verified Depth-First Algorithms

10.29007/8hkx ◽  
2018 ◽  
Author(s):  
René Neumann

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.

2021 ◽  
Author(s):  
Giuseppe De Giacomo ◽  
Antonio Di Stasio ◽  
Giuseppe Perelli ◽  
Shufang Zhu

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.


Author(s):  
Keijo Heljanko ◽  
Tommi Junttila ◽  
Misa Keinänen ◽  
Martin Lange ◽  
Timo Latvala

Author(s):  
Simon Jantsch ◽  
David Müller ◽  
Christel Baier ◽  
Joachim Klein

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.


2014 ◽  
Vol 131 (1) ◽  
pp. 27-53 ◽  
Author(s):  
Sami Evangelista ◽  
Lars Michael Kristensen

Sign in / Sign up

Export Citation Format

Share Document