Tehran Institute for Advanced Studies (TEIAS)

/ A Myhill-Nerode Theorem for Register Automata and Symbolic Trace Languages

Talk

A Myhill-Nerode Theorem for Register
Automata and Symbolic Trace Languages

October 14, 2020
(23 Mehr, 1399)

Venue

This Talk is online

+982189174612

Frits Vaandrager

Professor of Informatics for Technical Applications, Radboud University, Netherlands

Overview

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 equivalence relations to capture the additional structure of register automata. 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. We believe that moving to a grey-box settstate-of-the-art black-box learning algorithms.

Biography

Frits W.Vaandrager is Professor of Informatics for Technical Applications, Institute for Computing and Information Sciences, Radboud University, Nijmegen. Frits earned his M.S. in Mathematics with specialization in Computer Science at the University of Leiden in 1985 with the thesis “Algebraic techniques for concurrency and their application”. He earned his Ph.D. in Computer Science at the University of Amsterdam in 1990 with the thesis “Verification of two communication protocols by means of process algebra”. Frits has a strong interest in the development and application of theory, (formal) methods and tools for the speciation and analysis of computer based systems. In particular, he is interested in real-time embedded systems, distributed algorithms and protocols.