Abstract

Traditional computer science is Boolean: a Turing machine accepts or rejects its input, and logic assertions are true or false. A primary use of logic in computer science has been the specification and verification of reactive systems. There, desired behaviors of systems are formally specified by temporal-logic formulas, and questions about systems and their behaviors are reduced to questions like satisfiability and model checking. While correctness is binary, many questions we want to ask about systems are multi-valued. The multivalued setting arises directly in systems with quantitative aspects, for example systems with fuzzy assignments or stochastic dynamics, and arises also in Boolean systems, where it origins from the semantics of the specification formalism. In particular, beyond checking whether a system satisfies its specification, we may want to evaluate the quality in which the specification is satisfied. The term “quality” may refer to many aspects of the behavior: we may want to prioritize different satisfaction alternatives, refer to delays, costs, and many more. In recent years, we have seen a growing effort in the formal-method community to shift from Boolean specification formalisms to multi-valued ones. The shift involves a development of multi-valued temporal logics as well as algorithms and tools for reasoning about such logics.

This survey describes the basics of specification and verification of reactive systems, and the automata-theoretic approach for them: by translating temporal-logic formulas to automata, one reduces questions like satisfiability and model checking to decision problems on automata, like nonemptiness and language containment.

We first describe the Boolean setting: temporal logics, and their applications in specification and verification. Since we care about on-going behaviors of non-terminating systems, the formalisms we study specify infinite computations, and we focus on the theoretical properties of automata on infinite words. The transition from finite to infinite words results in a beautiful mathematical model with much richer combinatorial properties. We then describe two multi-valued settings. The first is based on finite lattices and the second on arbitrary functions over [0, 1]. In both settings, the goal is to refine the Boolean correctness query to a quantitative-evaluation query. Accordingly, the formalisms we introduce are such that the satisfaction value of a temporal-logic formula in a model, or the membership value of a word in the language of an automaton, are multi valued, and classical decision problems become search problems.

Multi-Valued Reasoning about Reactive Systems

Traditionally computer science has been Boolean in nature giving rise to systems based on proving correctness. Correctness is binary, but many questions we want to ask about systems are multi-valued. In modern computing systems this is becoming increasingly insufficient. In particular, beyond checking whether a system satisfies its specification, we may want to evaluate the quality in which the specification is satisfied. This has led to a shift from Boolean specification formalisms to multi-valued ones, which involves a development of multi-valued temporal logics as well as algorithms and tools for reasoning about such logics.

This timely in-depth review describes the basics of specification and verification of reactive systems, and the automata-theoretic approach for them: by translating temporal-logic formulas to automata.

As introductory material, the author describes the Boolean setting in which the formalisms specify infinite computations. This begins with linear temporal logic, and then focusses on automata on infinite words and their theoretical properties. The author then shows how to refine the Boolean correctness query by a quantitative one in two multi-valued settings. The formalisms introduced are such that the satisfaction value of a temporal-logic formula in a computation, or the membership value of a word in the language of an automaton, are multi valued, and classical decision problems become search problems.

Multi-Valued Reasoning about Reactive Systems is a concise source for all researchers and students wishing to understand quickly the theory behind the topic and the context it has within the wider active research branch.