Massimo Benerecetti

Massimo Benerecetti, Marco Faella, Stefano Minopoli

In this paper we study the problem of automatically generating switching controllers for the class of Linear Hybrid Automata, with respect to safety objectives. We identify and solve inaccuracies contained in previous characterizations of the problem, providing a sound and complete symbolic fixpoint procedure, based on polyhedral abstractions of the state space. We also prove the termination of each iteration of the procedure. Some promising experimental results are presented, based on an implementation of the fixpoint procedure on top of the tool PHAVer.

Massimo Benerecetti, Dario Della Monica, Angelo Matteo et al.

We study the expressive power of First-Order Logic (\FO) over (unordered) infinite trees, with the aim of identifying robust characterisations in terms of branching-time specification formalisms. While such correspondences are well understood in the linear-time setting, the branching-time case presents well-known structural challenges. To this end, we introduce two classes of hesitant tree automata and show that they capture precisely the expressive power of two branching-time temporal logics, namely \PolPCTL and \CTLsf, both of which have been previously shown to be equivalent to \FO over infinite trees. These results provide uniform automata-theoretic characterisations and yield a natural normal form for the latter in terms of a new fragment of \CTLs called \PolCTLs. As a consequence, we identify a fundamental limitation of \FO in this setting: along each branch, it can express only properties that are either safety or co-safety, thereby revealing a sharp expressive boundary for first-order definability over infinite trees.