The general subject of the research carried on is automaton-theoretic modeling of distributed and real-time systems. The most recent results regard probability and security for these systems.
The role of automata for analysing properties of systems is widely recognised. In recent years classes of automata for the specification and verification of real-time systems have been introduced both with discrete time and with dense time assumption (e.g. Timed Automata, Timed Cooperating Automata, Timed Automata with Non-instantaneous Actions, Hybrid Automata).
Explicit representation of time seems to be essential for specifying and verifying many systems. Among these there are: control systems, smart cards, communications by mobile phones, transactions via web.
It is also interesting the use of automata to model probabilistic aspects of the system under consideration, possibly towards the end of specifying and verifying properties.
Many complex systems have a hierarchical structure, and thus this structure should also be a feature of formalisms, in order to ensure an adequate modelling. The feature of hierarchy together with the ability of representing parallel composition came to prominence in Finite State Machines with the introduction of the specification formalism Statecharts and has been adopted in many specification formalisms, such as Modecharts and Rsml, and are a central component of various object oriented software development methodologies (e.g. see the Unified Modelling Language).
In multilevel systems it is important to avoid unwanted indirect information flow from higher levels to lower levels, namely the so called covert channels. Initial studies of information flow analysis were performed by abstracting away from time and probability. It is already known that systems that are considered to be secure may turn out to be insecure when time or probability are considered. Recently, work has been done in order to consider also asp