Author name cluster

Frits Vaandrager

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

11 papers

1 author row

I&C Journal 2023 Journal Article

Learning Mealy machines with one timer

Frits Vaandrager
Masoud Ebrahimi
Roderick Bloem

We present Mealy machines with a single timer (MM1Ts), a class of sufficiently expressive models to describe the real-time behavior of many realistic applications that we can learn efficiently. We show how we can obtain learning algorithms for MM1Ts via a reduction to the problem of learning Mealy machines. We describe an implementation of an MM1T learner on top of LearnLib and compare its performance with recent algorithms proposed by Aichernig et al. and An et al. on several realistic benchmarks.

Details DOI

TCS Journal 2022 Journal Article

A Myhill-Nerode theorem for register automata and symbolic trace languages

Frits Vaandrager
Abhisek Midya

We propose a new symbolic trace semantics for register automata (extended finite state machines) which records both the sequence of input symbols that occur during a run as well as the constraints on input parameters that are imposed by this run. Our main result is a generalization of the classical Myhill-Nerode theorem to this symbolic setting. Our generalization requires the use of three relations to capture the additional structure of register automata. Location equivalence ≡ l captures that symbolic traces end in the same location, transition equivalence ≡ t captures that they share the same final transition, and a partial equivalence relation ≡ r captures that symbolic values v and v ′ are stored in the same register after symbolic traces w and w ′, respectively. A symbolic language is defined to be regular if relations ≡ l, ≡ t and ≡ r exist that satisfy certain conditions, in particular, they all have finite index. We show that the symbolic language associated to a register automaton is regular, and we construct, for each regular symbolic language, a register automaton that accepts this language. Our result provides a foundation for grey-box learning algorithms in settings where the constraints on data parameters can be extracted from code using e. g. tools for symbolic/concolic execution or tainting. Moving to a grey-box setting may overcome the scalability problems of state-of-the-art black-box learning algorithms.

Details DOI

Highlights Conference 2017 Conference Abstract

Model learning

Frits Vaandrager

Model learning, a. k. a. active automata learning, is emerging as a effective technique for obtaining state machine models of software components. In this tutorial, I will give a brief introduction to the area, highlight how model learning helped to find standard violations in implementations of the TCP, TLS and SSH protocols, and discuss recent work on the use of SMT solvers for model learning and algorithms for model learning of timed systems.

Details

TCS Journal 2012 Journal Article

Analysis of a clock synchronization protocol for wireless sensor networks

Faranak Heidarian
Julien Schmaltz
Frits Vaandrager

The Dutch company Chess develops a wireless sensor network (WSN) platform using an epidemic communication model. One of the greatest challenges in the design is to find suitable mechanisms for clock synchronization. In this paper, we study a proposed clock synchronization protocol for the Chess platform. First, we model the protocol as a network of timed automata and verify various instances using the Uppaal model checker. Next, we present a full parametric analysis of the protocol for the special case of cliques (networks with full connectivity), that is, we give constraints on the parameters that are both necessary and sufficient for correctness. These results have been checked using the proof assistant Isabelle. We report on the exhaustive analysis of the protocol for networks with four nodes, and we present a negative result for the special case of line topologies: for any instantiation of the parameters, the protocol will eventually fail if the network grows.

Details DOI

TCS Journal 2006 Journal Article

Switched PIOA: Parallel composition via distributed scheduling

Ling Cheung
Nancy Lynch
Roberto Segala
Frits Vaandrager

This paper presents the framework of switched probabilistic input/output automata (or switched PIOA), augmenting the original PIOA framework with an explicit control exchange mechanism. Using this mechanism, we model a network of processes passing a single token among them, so that the location of this token determines which process is scheduled to make the next move. This token structure therefore implements a distributed scheduling scheme: scheduling decisions are always made by the (unique) active component. Distributed scheduling allows us to draw a clear line between local and global nondeterministic choices. We then require that local nondeterministic choices are resolved using strictly local information. This eliminates unrealistic schedules that arise under the more common centralized scheduling scheme. As a result, we are able to prove that our trace-style semantics is compositional.

Details DOI

I&C Journal 2003 Journal Article

Hybrid I/O automata

Nancy Lynch
Roberto Segala
Frits Vaandrager

Hybrid systems are systems that exhibit a combination of discrete and continuous behavior. Typical hybrid systems include computer components, which operate in discrete program steps, and real-world components, whose behavior over time intervals evolves according to physical constraints. Important examples of hybrid systems include automated transportation systems, robotics systems, process control systems, systems of embedded devices, and mobile computing systems. Such systems can be very complex, and very difficult to describe and analyze. This paper presents the Hybrid Input/Output Automaton (HIOA) modeling framework, a basic mathematical framework to support description and analysis of hybrid systems. An important feature of this model is its support for decomposing hybrid system descriptions. In particular, the framework includes a notion of external behavior for a hybrid I/O automaton, which captures its discrete and continuous interactions with its environment. The framework also defines what it means for one HIOA to implement another, based on an inclusion relationship between their external behavior sets, and defines a notion of simulation, which provides a sufficient condition for demonstrating implementation relationships. The framework also includes a composition operation for HIOAs, which respects the implementation relation and a notion of receptiveness, which implies that an HIOA does not block the passage of time. The framework is intended to support analysis methods from both computer science and control theory. This work is a simplification of our earlier HIOA model. The main simplification in the new model is a clearer separation between the mechanisms used to model discrete and continuous interaction between components. In particular, the new model removes the dual use of external variables for discrete and continuous interactions.

Details DOI

TCS Journal 2001 Journal Article

Testing timed automata

Jan Springintveld
Frits Vaandrager
Pedro R. D'Argenio

We present a generalization of the classical theory of testing for Mealy machines to a setting of dense real-time systems. A model of timed I/O automata is introduced, inspired by the timed automaton model of Alur and Dill, together with a notion of test sequence for this model. Our main contributions is a test suite derivation algorithm for black-box conformance testing of timed I/O automata. Black-box testing amounts to checking whether an implementation conforms to a specification of its external behavior, by means of a set of tests derived solely from specification. The main problem is to derive a finite set of tests from a possibly infinite, dense time transition system representing the specification. The solution is to reduce the dense time transition system to an appropriate finite discrete subautomaton, the grid automaton, which contains enough information to completely represent the specification from a test perspective. Although the method results in a test suite of high exponential size and cannot be claimed to be of practical value, it gives the first algorithm that yields a finite and complete set of tests for dense real-time systems.

Details DOI

I&C Journal 1997 Journal Article

The Difference between Splitting innandn+1

Rob van Glabbeek
Frits Vaandrager

It is established that durational and structural aspects of actions can in general not be modeled in standard interleaving semantics, even when a time-consuming action is represented by a pair of instantaneous actions denoting its start and finish. By means of a series of counterexamples it is shown that, for anyn, it makes a difference whether actions are split innor inn+1 parts.

Details DOI

I&C Journal 1996 Journal Article

Forward and Backward Simulations

Nancy Lynch
Frits Vaandrager

A general automaton model for timing-based systems is presented and is used as the context for developing a variety of simulation proof techniques for such systems. These techniques include (1) refinements, (2) forward and backward simulations, (3) hybrid forward–backward and backward–forward simulations, and (4) history and prophecy relations. Relationships between the different types of simulations, as well as soundness and completeness results, are stated and proved. These results are (with one exception) analogous to the results for untimed systems in Part I of this paper. In fact, many of the results for the timed case are obtained as consequences of the analogous results for the untimed case.

Details DOI

TCS Journal 1993 Journal Article

Modular specification of process algebras

Rob van Glabbeek
Frits Vaandrager

This paper proposes a modular approach to the algebraic specification of process algebras. This is done by means of the notion of a module. The simplest modules are building blocks of operators and axioms, each block describing a feature of concurrency in a certain semantical setting. These modules can then be combined by means of a union operator +, an export operator □, allowing to forget some operators in a module, an operator H, changing semantics by taking homomorphic images, and an operator S which takes subalgebras. These operators enable us to combine modules in a subtle way, when the direct combination would be inconsistent. We give a presentation of equational logic, infinitary conditional equational logic — of which we also prove the completeness — and first-order logic and show how the notion of a formal proof of a formula from a theory can be generalized to that of a proof of a formula from a module. This module logic is then applied in process algebra. We show how auxiliary process algebra operators can be hidden when this is needed. Moreover, we demonstrate how new process combinators can be defined in terms of more elementary ones in a clean way. As an illutration of our approach, we specify some FIFO-queues and verify several of their properties.

Details DOI

I&C Journal 1992 Journal Article

Structured operational semantics and bisimulation as a congruence

Jan Friso Groote
Frits Vaandrager

In this paper we are interested in general properties of classes of transition system specifications in Plotkin style. The discussion takes place in a setting of labelled transition systems. The states of the transition systems are terms generated by a single sorted signature and the transitions between states are defined by conditional rules over the syntax. It is argued that in this setting it is natural to require that strong bisimulation equivalence be a congruence on the states of the transition systems. A general format, called the tyft/tyxt format, is presented for the rules in a transition system specification, such that bisimulation is always a congruence when all the rules fit this format. With a series of examples it is demonstrated that the tyft/tyxt format cannot be generalized in any obvious way. Another series of examples illustrates the usefulness of our congruence theorem. Briefly we touch upon the issue of modularity of transition system specifications. It is argued that certain pathological tyft/tyxt rules (the ones which are not pure) can be disqualified because they behave badly with respect to modularization. Next we address the issue of full abstraction. We characterize the completed trace congruence induced by the operators in pure tyft/tyxt format as 2-nested simulation equivalence. The pure tyft/tyxt format includes the format given by de Simone (Theoret. Comput. Sci. 37, 245–267 (1985)) but is incomparable to the GSOS format of Bloom, Istrail, and Meyer (in “Conference Record of the 15th Annual Symposium on Principles of Programming Languages, San Diego, California, 1988, ” pp. 229–239). However, it turns out that 2-nested simulation equivalence strictly refines the completed trace congruence induced by the GSOS format.

Details DOI