Regular expressions for timed automata

Abstract

Finite automata are valuable models for various types of software, such as system verifica-tion software and text search software, etc. A widely acclaimed result in computer science is the proof that finite automata can be represented through a notation structure called a regular expression. This means that regular expressions succeed in describing the same patterns that can be represented by a finite automaton. We know that it is difficult to prove that two finite automata are equivalent. Still, by converting them to a regular expression, you can determine relatively easily whether they represent the same language. Timed automata are an extension of finite automata with a finite set of clocks. Timed automata are widely used in model checking and also in real-time systems such as commu-nication and security protocols. In recent years there is an increasing demand for this type of software. As in classical automata, timed automata can also be represented by regular expressions. However, so far, there is no conversion software developed. There are two main methods for converting: the state elimination method; and the Brzozowski's method. These methods refer to the classic automaton model. The goal of this work is the study and development of an algorithm that converts a timed automaton into a timed regular expression. For this, i) we developed a conversion al-gorithm based on Brzozowski's method for timed automata adding to the classical case several changes, in particular, the incorporation of clocks and transition restrictions, among other, 2) we developed a software tool that converts a timed regular expression into a timed automaton, and depicting both of them.

Autómatos finitos são modelos úteis para vários tipos de software, tais como, software de verificação de sistemas e software de pesquisa de texto, etc. Um resultado amplamente aclamado na ciência da computação é a prova de que autómatos finitos podem ser repre-sentados através de uma estrutura de notação chamada expressão regular. Estas expressões regulares conseguem descrever os mesmos padrões que podem ser representados por um autómato finito. Sabemos que é difícil provar que dois autómatos finitos são equivalentes, mas ao converte-los para uma expressão regular consegue-se determinar com relativa facil-idade se eles representam a mesma linguagem. Os autómatos temporais são uma extensão de autómatos finitos com um conjunto finito de relógios. Os autómatos temporais são muito usados em model cheking e também em sis-temas de tempo-real, como protocolos de comunicação e segurança. Nos últimos anos tem havido procura crescente para esse tipo de software. Tal como nos autómatos clássicos, os autómatos temporais podem ser representados por expressões regulares. Mas até agora não existe software de conversão desenvolvido. Existem dois métodos principais para efetuar a conversão: método de eliminação de estados; e o método de Brzozowski. Estes métodos funcionam para o modelo clássico de autómato. O objetivo deste trabalho é o estudo e desenvolvimento de um algoritmo que converta um autómato temporal numa expressão regular. Para isso, i) desenvolvemos um algoritmo de conversão baseado no método de Brzozowski, incorporando diversos elementos adiciona-dos, nomeadamente, relógios e restrições nas transições, entre outras 2) desenvolvemos uma ferramenta que converte uma expressão regular temporal num autómato temporal, e no final estes dois elementos são representados numa única imagem.