From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata

Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper, we describe a single exponential translation from limit-deterministic Büchi automata (LDBA) to DPA and show that it can be concatenated with a recent efficient translations from LTL to LDBA to yield a double exponential, ‘Safraless’ LTL-to-DPA construction. We also report on an implementation and a comparison with other LTL-to-DPA translations on several sets of formulas from the literature.

     

Efficient emptiness check for timed Büchi automata

The Büchi non-emptiness problem for timed automata refers to deciding if a given automaton has an infinite non-Zeno run satisfying the Büchi accepting condition. The standard solution to this problem involves adding an auxiliary clock to take care of the non-Zenoness. In this paper, it is shown that this simple transformation may sometimes result in an exponential blowup. A construction avoiding this blowup is proposed. It is also shown that in many cases, non-Zenoness can be ascertained without an extra construction. An on-the-fly algorithm for the non-emptiness problem, using a non-Zenoness construction only when required, is proposed. Experiments carried out with a prototype implementation of the algorithm are reported.     

B��chi automata for modeling component connectors

Reo is an exogenous coordination language for component connectors extending data flow networks with synchronization and context-dependent behavior. The first proposed formalism to capture the operational semantics of Reo is called constraint automaton. In this paper, we propose another operational model of Reo based on Büchi automata in which port synchronization is modeled by records labeling the transitions, whereas context dependencies are stored in the states. It is shown that constraint automata can be recast into our proposed Büchi automata of records. Also, we provide a composition operator which models the joining of two connectors and show that it can be obtained by using two standard operators: alphabet extension and automata product. Our semantics has the advantage over previous models in that it is based on standard automata theory, so that existing theories and tools can be easily reused. Moreover, it is the first formal model addressing all of Reo’s features: synchronization, mutual exclusion, hiding, and context-dependency.     

Variations on parallel explicit emptiness checks for generalized Büchi automata

We present new parallel explicit emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on a strongly connected component (SCC) enumeration and support generalized Büchi acceptance, and require no synchronization points or recomputing procedures. A salient feature of our algorithms is the use of a global union-find data structure in which multiple threads share structural information about the automaton checked. Besides these basic algorithms, we present one architectural variant isolating threads that write to the union-find, and one extension that decomposes the automaton based on the strength of its SCCs to use more optimized emptiness checks. The results from an extensive experimentation of our algorithms and their variations show encouraging performances, especially when the decomposition technique is used.     

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

Formal Methods in System Design - Due to the high complexity of translating linear temporal logic (LTL) to deterministic automata, several forms of “restricted” nondeterminism have been...     

Efficient approach of translating LTL formulae into Büchi automata

In explicit-state model checking, system properties are typically expressed in linear temporal logic (LTL), and translated into a Büchi automaton (BA) to be checked. In order to improve performance of the conversion algorithm, some model checkers involve the intermediate automata, such as a generalized Büchi automaton (GBA). The de-generalization is a translation from a GBA to a BA. In this paper, we present a conversion algorithm to translate an LTL formula to a BA directly. A labeling, acceptance degree, is presented to record acceptance conditions satisfied in each state and transition. Acceptance degree is a set of U-subformulae or F-subformulae of the given LTL formula. According to the acceptance degree, on-the-fly degeneralization algorithm, which is different from the standard de-generalization algorithm, is conceived and implemented. On-the-fly de-generalization algorithm is carried out during the expansion of the given LTL formula. It is performed in the case of the given LTL formula contains U-subformulae and F-subformulae, that is, the on-the-fly de-generalization algorithm is performed as required. In order to get a more deterministic BA, the shannon expansion is used recursively during expanding LTL formulae. Ordered binary decision diagrams are used to represent the BA and simplify LTL formulae.We compare the conversion algorithm presented in this paper to previousworks, and show that it is more efficient for five families LTL formulae in common use and four sets of random formulae generated by LBTT (an LTL-to-Büchi translator testbench).     

Büchi context-free languages

We define context-free grammars with Büchi acceptance condition generating languages of countable words. We establish several closure properties and decidability results for the class of Büchi context-free languages generated by these grammars. We also define context-free grammars with Müller acceptance condition and show that there is a language generated by a grammar with Müller acceptance condition which is not a Büchi context-free language.     

从基于迁移的扩展Büchi自动机到Büchi自动机

目前的模型检测方法中,有一种方法是基于自动机来实现的.具体做法是:将抽象出的系统模型用Büchi自动机来表示,将需要验证的性质用LTL(linear temporal logic)公式来表达;然后将LTL公式取反后转化为Büchi自动机,并检查这两个自动机接受语言之间的包含关系.有一类LTL公式转化为Büchi自动机的算法是:在计算过程中,首先得到一个标注在迁移上的扩展Büchi自动机(transition-based generalized Büchi automaton,简称TGBA),然后把这种扩展Büchi自动机转换成非扩展的Büchi自动机.针对这类转换算法,根据Büchi自动机接受语言的特点,重新定义了基于迁移的扩展Büchi自动机的求交运算,减少了需要复制的状态个数,使转换后的自动机具有较少的状态.测试的结果表明:对随机产生的公式,新算法相对于以往的算法有明显的优势.     

Advances in probabilistic model checking with PRISM: variable reordering,quantiles and weak deterministic Büchi automata

International Journal on Software Tools for Technology Transfer - The popular model checker PRISM has been successfully used for the modeling and analysis of complex probabilistic systems. As one...     

An input–output simulation approach to controlling multi-affine systems for linear temporal logic specifications

This article presents an input–output simulation approach to controlling multi-affine systems for linear temporal logic (LTL) specifications, which consists of the following steps. First, the state space is partitioned into rectangles, each of which satisfies atomic LTL propositions. Then, we study the control of multi-affine systems on rectangles, including the control based on the exit sub-region to drive all trajectories starting from a rectangle to exit through a facet and the control to stabilise the multi-affine system towards a desired point. With the proposed controllers, a finitely abstracted transition system is constructed which is shown to be input–output simulated by the rectangular transition system of the multi-affine system. Since the input–output simulation preserves LTL properties, the controller synthesis of the multi-affine system for LTL specifications is achieved by designing a nonblocking supervisor for the abstracted transition system and by implementing the resulting supervisor to the original multi-affine system.     

模糊Büchi自动机的等价刻画

模糊语言的研究是形式语言研究的焦点之一,然而如何对模糊语言进行刻画甚至更好地分类是其中一个重要研究方向.文章在模糊ω-语言的研究基础上,从模糊逻辑角度研究了模糊ω-正则语言的等价刻画.首先借助广义子集构造方法,证明了任一模糊Büchi自动机与具有分明初始状态和状态转移函数且具有模糊终状态的模糊Büchi自动机是等价的,藉此研究了模糊ω-正则语言的代数刻画和层次刻画,讨论了模糊ω-正则语言关于正则运算的封闭性;其次引入单体二阶(L)ukasiewicz逻辑的概念,给出模糊Büchi自动机识别语言的等价逻辑刻画;最后通过引入ω-星自由和ω-非周期模糊ω-语言,利用“层次化”处理技巧得到了多值逻辑意义下的分类定理,对模糊ω-正则语言给出了一种分类方法.     

Checking Timed Büchi Automata Emptiness Efficiently

This paper presents an on-the-fly and symbolic technique for efficiently checking timed automata emptiness. It is symbolic because it uses the simulation graph (instead of the region graph). It is on-the-fly because the simulation graph is generated during the test for emptiness. We have implemented a verification tool called Profounder based on this technique. To our knowledge, Profounder is the only available tool for checking emptiness of timed Büchi automata. To illustrate the practical interest of our approach, we show the performances of the tool on a non-trivial case study.     

The complexity of the temporal logic with “until” over general linear time

It is shown that the decision problem for the temporal logic with the strict until operator over general linear time is PSPACE-complete. This shows that it is no harder to reason with arbitrary linear orderings than with discrete linear time temporal logics. New techniques are used to give a PSPACE procedure for the logic.     

Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives

We consider Markov decision processes (MDPs) with Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure winning states from where the objective can be ensured with probability 1. Our contributions are as follows: First, we present the first subquadratic symbolic algorithm to compute the almost-sure winning set for MDPs with Büchi objectives; our algorithm takes $O(n \cdot\sqrt{m})$ symbolic steps as compared to the previous known algorithm that takes O(n ²) symbolic steps, where n is the number of states and m is the number of edges of the MDP. In practice MDPs have constant out-degree, and then our symbolic algorithm takes $O(n \cdot\sqrt{n})$ symbolic steps, as compared to the previous known O(n ²) symbolic steps algorithm. Second, we present a new algorithm, namely win-lose algorithm, with the following two properties: (a) the algorithm iteratively computes subsets of the almost-sure winning set and its complement, as compared to all previous algorithms that discover the almost-sure winning set upon termination; and (b) requires $O(n \cdot\sqrt{K})$ symbolic steps, where K is the maximal number of edges of strongly connected components (scc’s) of the MDP. The win-lose algorithm requires symbolic computation of scc’s. Third, we improve the algorithm for symbolic scc computation; the previous known algorithm takes linear symbolic steps, and our new algorithm improves the constants associated with the linear number of steps. In the worst case the previous known algorithm takes 5?n symbolic steps, whereas our new algorithm takes 4?n symbolic steps.     

Schützenberger and Eilenberg theorems for words on linear orderings

This paper contains extensions to words on countable scattered linear orderings of two well-known results of characterization of languages of finite words. We first extend a theorem of Schützenberger establishing that the star-free sets of finite words are exactly the languages recognized by finite aperiodic semigroups. This gives an algebraic characterization of star-free sets of words over countable scattered linear orderings. Contrarily to the case of finite words, first-order definable languages are strictly included into the star-free languages when countable scattered linear orderings are considered. Second, we extend the variety theorem of Eilenberg for finite words: there is a one-to-one correspondence between varieties of languages of words on countable scattered linear orderings and pseudo-varieties of algebras. The star-free sets are an example of such a variety of languages.     

Filter-based iterative learning control for linear large-scale industrial processes

In the procedure of the steady-state hierarchical optimization with feedback for large-scale industrial processes, a sequence of set-point changes with different magnitudes is carried out on the optimization layer. To improve the dynamic performance of transient response driven by the set-point changes, a filter-based iterative leaning control strategy is proposed. In the proposed updating law, a local-symmetric-integral operator is adopted for eliminating the measurement noise of output information, a set of desired trajectories are specified according to the set-point changes sequence, the current control input is iteratively achieved by utilizing smoothed output error to modify its control input at previous iteration, to which the amplified coefficients related to the different magnitudes of set-point changes are introduced. The convergence of the algorithm is conducted by incorporating frequency-domain technique into time-domain analysis. Numerical simulation demonstrates the effectiveness of the proposed strategy.     

Boosting learning and inference in Markov logic through metaheuristics

Markov Logic (ML) combines Markov networks (MNs) and first-order logic by attaching weights to first-order formulas and using these as templates for features of MNs. State-of-the-art structure learning algorithms in ML maximize the likelihood of a database by performing a greedy search in the space of structures. This can lead to suboptimal results because of the incapability of these approaches to escape local optima. Moreover, due to the combinatorially explosive space of potential candidates these methods are computationally prohibitive. We propose a novel algorithm for structure learning in ML, based on the Iterated Local Search (ILS) metaheuristic that explores the space of structures through a biased sampling of the set of local optima. We show through real-world experiments that the algorithm improves accuracy and learning time over the state-of-the-art algorithms. On the other side MAP and conditional inference for ML are hard computational tasks. This paper presents two algorithms for these tasks based on the Iterated Robust Tabu Search (IRoTS) metaheuristic. The first algorithm performs MAP inference and we show through extensive experiments that it improves over the state-of-the-art algorithm in terms of solution quality and inference time. The second algorithm combines IRoTS steps with simulated annealing steps for conditional inference and we show through experiments that it is faster than the current state-of-the-art algorithm maintaining the same inference quality.     

A Kleene–Schützenberger theorem for weighted timed automata

During the last years, weighted timed automata have received much interest in the real-time community. Weighted timed automata form an extension of timed automata and allow us to assign weights (costs) to both locations and edges. This model, introduced by Alur et al. (2001) and Behrmann et al. (2001), permits the treatment of continuous consumption of resources and has led to much research on scheduling problems, optimal reachability and model checking. Also, several authors have derived Kleene-type characterizations of (unweighted) timed automata and their accepted timed languages. The goal of this paper is to provide a characterization of the behaviours of weighted timed automata by rational power series. We define weighted timed automata with weights taken in an arbitrary semiring, resulting in a model that subsumes several weighted timed automata concepts of the literature. For our main result, we combine the methods of Schützenberger, a recent approach for a Kleene-type theorem for unweighted timed automata by Bouyer and Petit as well as new techniques. Our main result also implies Kleene-type theorems for several subclasses of weighted timed automata investigated before, e.g., for timed automata and timed automata with stopwatch observers.     

Pointfree expression and calculation: from quantification to temporal logic

Pointfree formulation means suppressing domain variables to focus on higher-level objects (functions, relations). Advantages are algebraic-style calculation and abstraction as formal logics pursue by axiomatization. Various specific uses are considered, starting with quantification in the wider sense (?, ?, ∑, etc.). Pointfree style is achieved by suitable functionals that prove superior to pointwise conventions such as the Eindhoven notation. Pointwise calculations from the literature are reworked in pointfree form. The second use considered is in describing systems, with generic functionals capturing signal flow patterns. An illustration is the mathematics behind a neat magician’s trick, whose implementation allows comparing the pointfree style in Funmath, LabVIEW, TLA⁺, Haskell and Maple. The third use is making temporal logic calculational, with a simple generic Functional Temporal Calculus (FTC) for unification. Specific temporal logics are then captured via endosemantic functions. The example is TLA⁺. Calculation is illustrated by deriving various theorems, most related to liveness issues, and discovering results by calculation rather than proving them afterwards. To conclude, various ramifications, style and abstraction issues are discussed, in relation to engineering mathematics in general and to categorical formulations.     

Büchi Store: an open repository of \omega -automata

We introduce Büchi Store, an open repository of Büchi automata and other types of $\omega $ -automata for model-checking practice, research, and education. The repository contains Büchi automata and their complements for common specification patterns and numerous temporal formulae. These automata are made as small as possible by various construction techniques in view of the fact that smaller automata are easier to understand and often help in speeding up the model-checking process. The repository is open, allowing the user to add automata that define new languages or are smaller than existing equivalent ones. Such a collection of Büchi automata is also useful as a benchmark for evaluating translation or complementation algorithms and as examples for studying Büchi automata and temporal logic. These apply analogously for other types of $\omega $ -automata, including deterministic Büchi and deterministic parity automata, which are also collected in the repository. In particular, the use of smaller deterministic parity automata as an intermediary helps reduce the complexity of automatic synthesis of reactive systems from temporal specifications.