Time for Verification

The traditional Dung networks depict arguments as atomic and studies the relationships of attack between them. This can be generalised in two ways. One is to consider, for example, various forms of attack, support and feedback. Another is to add content to nodes and put there not just atomic arguments but more structure, for example, proofs in some logic or simply just formulas from a richer language. This paper offers to use temporal and modal language formulas to represent arguments in the nodes of a network. The suitable semantics for such networks is Kripke semantics. We also introduce a new key concept of usability of an argument.

Priorities are used to control the execution of systems to meet given requirements for optimal use of resources, e.g., by using scheduling policies. For distributed systems it is hard to find efficient implementations for priorities; because they express constraints on global states, their implementation may incur considerable overhead.

Our method is based on performing model checking for knowledge properties. It allows identifying where the local information of a process is sufficient to schedule the execution of a high priority transition. As a result of the model checking, the program is transformed to react upon the knowledge it has at each point. The transformed version has no priorities, and uses the gathered information and its knowledge to limit the enabledness of transitions so that it matches or approximates the original specification of priorities.

While a boolean notion of correctness is given by a preorder on systems and properties, a quantitative notion of correctness is defined by a distance function on systems and properties, where the distance between a system and a property provides a measure of “fit” or “desirability.” In this article, we explore several ways how the simulation preorder can be generalized to a distance function. This is done by equipping the classical simulation game between a system and a property with quantitative objectives. In particular, for systems that satisfy a property, a quantitative simulation game can measure the “robustness” of the satisfaction, that is, how much the system can deviate from its nominal behavior while still satisfying the property. For systems that violate a property, a quantitative simulation game can measure the “seriousness” of the violation, that is, how much the property has to be modified so that it is satisfied by the system. These distances can be computed in polynomial time, since the computation reduces to the value problem in limit average games with constant weights. Finally, we demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.

Automated abstraction is widely recognized as a key method for computer-aided verification of hardware and software. In this paper, we describe the evolution of counterexample-guided refinement and other iterative abstraction refinement techniques.

The key to precision and scalability in all formal methods for static program analysis and verification is the handling of disjunctions arising in relational analyses, the flow-sensitive traversal of conditionals and loops, the context-sensitive inter-procedural calls, the interleaving of concurrent threads, etc. Explicit case enumeration immediately yields to combinatorial explosion. The art of scalable static analysis is therefore to abstract disjunctions to minimize cost while preserving weak forms of disjunctions for expressivity.

We propose a library based incremental design methodology for constructing hybrid controllers from a component library of models of hybrid controllers, such that global safety and stability properties are preserved. To this end, we propose hybrid interface specifications of components characterizing plant regions for which safety and stability properties are guaranteed, as well as exception mechanisms allowing safe and stability-preserving transfer of control whenever the plant evolves towards the boundary of controllable dynamics. We then propose a composition operator for constructing hybrid automata from a library of such pre-characterized components supported by compositional and automatable proofs of hybrid interface specifications.

A family of languages is called mildly context-sensitive if In our paper we introduce a new model of computation called buffer augmented pregroup grammars that defines a family of mildly context-sensitive languages. This model of computation is an extension of Lambek pregroup grammars with a variable symbol – the (buffer) and is allowed to make an arbitrary substitution from the original pregroup to the variable. This increases the pregroup grammar generation power, but still retains the desired properties of mildly context-sensitive languages such as semi-linearity and polynomial parsing. We establish a strict hierarchy within the family of mildly context-sensitive languages defined by buffer augmented pregroup grammars. In this hierarchy, the hierarchy level of the family language depends on the allowed number of occurrences of the variable in lexical category assignments.

We present two proof rules for the equivalence of recursive procedures, in the style of Hoare’s rule for recursive invocation of procedures. The first rule can be used for proving partial equivalence of programs; the second can be used for proving their mutual termination. There are various applications to these rules, such as proving backward compatibility.

This paper combines three topics to which Amir Pnueli contributed significantly: the semantics of languages for concurrency, the semantics of statecharts, and reactive and hybrid systems. It is also no accident that the main motivation of our paper comes from biological systems: in recent years Amir became interested in these too. In [KLH10] we introduced Biocharts, a fully executable, two-tier compound visual language for modeling complex biological systems. The high-level part of the language is a version of statecharts, which have been shown to be successful in software and systems engineering. These statecharts can then be combined with any appropriately well-defined language (preferably a diagrammatic one) for specifying the low-level dynamics of the biological pathways and networks. The purpose of [KLH10] was to present the main concepts through a biological example and to illustrate the feasibility and usefulness of the approach. Here we discuss some of the questions that arise when one attempts to provide a careful definition of the semantics of Biocharts. We also compare the main requirements needed in a language for modeling biology with the way statecharts are used in software and system engineering.

In one version of Gilbreath’s card trick, a deck of cards is arranged as a series of quartets, where each quartet contains a card from each suit and all the quartets feature the same ordering of the suits. For example, the deck could be a repeating sequence of spades, hearts, clubs, and diamonds, in that order, as in the deck below.

The deck is then cut into two (not necessarily equal) half-decks, possibly as \({\langle 5\spadesuit\rangle}, {\langle 3\heartsuit\rangle}, {\langle Q\clubsuit\rangle}, {\langle 8\diamondsuit\rangle}, {\langle K\spadesuit\rangle}\) and \({\langle 2\heartsuit\rangle}, {\langle 7\clubsuit\rangle}, {\langle 4\diamondsuit\rangle}, {\langle 8\spadesuit\rangle}, {\langle J\heartsuit\rangle}, {\langle 9\clubsuit\rangle}, {\langle A\diamondsuit\rangle}\).

The order of one of the half-decks is then reversed. Either half-deck could be reversed. We can pick the smaller one, i.e., the first one, and reverse it to obtain \({\langle K\spadesuit\rangle}, {\langle 8\diamondsuit\rangle}, {\langle Q\clubsuit\rangle}, {\langle 3\heartsuit\rangle}, {\langle 5\spadesuit\rangle}\). The two half-decks are then shuffled in a (not necessarily perfect) riffle-shuffle. One such shuffle is shown below, where the underlined cards are drawn from the second half-deck.

The quartets in the shuffled deck are displayed to demonstrate that each quartet contains a card from each suit. This turns out to be inevitable no matter how the original deck is cut and the order in which the two decks are shuffled. The principle underlying the card trick can be proved in a number of ways. We present the argument as a series of transformations that demystify the trick and describe its formalization.

In this paper we develop an automata-theoretic framework for reasoning about infinite-state sequential systems. Our framework is based on the observation that states of such systems, which carry a finite but unbounded amount of information, can be viewed as nodes in an infinite tree, and transitions between states can be simulated by finite-state automata. Checking that a system satisfies a temporal property can then be done by an alternating two-way tree automaton that navigates through the tree. We show how this framework can be used to solve the model-checking problem for μ-calculus and LTL specifications with respect to pushdown and prefix-recognizable systems. In order to handle model checking of linear-time specifications, we introduce and study path automata on trees. The input to a path automaton is a tree, but the automaton cannot split to copies and it can read only a single path of the tree.

As has been the case with finite-state systems, the automata-theoretic framework is quite versatile. We demonstrate it by solving the realizability and synthesis problems for μ-calculus specifications with respect to prefix-recognizable environments, and extending our framework to handle systems with regular labeling regular fairness constraints and μ-calculus with backward modalities.

The Krohn-Rhodes theorem states that any deterministic automaton is a homomorphic image of a cascade of very simple automata which realize either resets or permutations. Moreover, if the automaton is counter-free, only reset automata are needed. In this paper we give a very constructive proof of a variant of this theorem due to Eilenberg.

Nearly twenty years ago, Amir and I (ZM) decided to write a series of three volumes summarizing the state of the art (at that time) on the verification of Reactive Systems using Temporal Logic techniques.

The concepts of temporal logic were introduced by Amir Pnueli [1] into the realm of computer science in general and programs in particular, to great effect. Given a program specification, a crucial element of reasoning through temporal logic is our ability to assert that one program event occurs before or after the other, with an order intuitively rooted in our notion of “time”. In the realm of temporal logic, such assertions are abstracted as pure mathematical facts. An alternative is to consider the physical realization by executing the specified program through, for example, a microprocessor-based system. In such a case, a mechanism is used to ensure that the desired temporal relationships from the program specification are obeyed, and quite often this mechanism takes the form of a clock. In physical instantiations however clocks and similar mechanisms have an associated energy cost. They are guided by the laws of physics in general and thermodynamics in particular, with which the arrow of time and the associated irreversibility are intimately intertwined. Viewed through this lens, a key question arises of whether the need for ensuring that the temporal norms needed for program correctness accrue an inevitable energy cost. In this paper, I sketch some of the intricacies underlying this question. I will hint at the subtle interactions between models of computing, time as it is represented in them, and the associated thermodynamic cost. In his early work, Amir relied as much on the philosophy of reasoning about time [2-4] as on the technical intricacies of mathematical logic. In recognition of the richness of his intellectual endeavor, I have developed this exposition in a philosophical style mimicking that of the ancient greek philosopher Zeno [5,6].

In their seminal 1991 paper “What is in a Step: On the Semantics of Statecharts”, Pnueli and Shalev showed how, in the presence of global consistency and while observing causality, the synchronous language Statecharts can be given coinciding operational and declarative step semantics. Over the past decade, this semantics has been supplemented with order-theoretic, denotational, axiomatic and game-theoretic characterisations, thus revealing itself as a rather canonical interpretation of the synchrony hypothesis.

In this paper, we survey these characterisations and use them to emphasise the close but not widely known relations of Statecharts to the synchronous language Esterel and to the field of logic programming. Additionally, we highlight some early reminiscences on Amir Pnueli’s contributions to characterise the semantics of Statecharts.