International audience

Hierarchical state machines represent a natural and useful framework to model and reason about modern systems. These machines encompass the ability to model hierarchical systems where some of the components can be reused in different contexts, e.g., by hierarchically calling subsystems. However, classical model checkers lack support to properly deal with hierarchical systems. Mostly, they treat the hierarchical calls as generic, possibly recursive, procedure calls. In this paper, we present HYASM a model checker for hierarchical systems as an extension of the tool YASM, a symbolic model-checker based on the CEGAR paradigm. Our tool uses a suitable flattening approach over hierarchical state machines, and experimental results show that our approach works very well in practice.

Action models of Dynamic Epistemic Logic (DEL) represent precisely how actions are perceived by agents. DEL has recently been used to define infinite multi-player games, and it was shown that they can be solved in some cases. However, the dynamics being defined by the classic DEL update product for individual actions, only turn-based games have been considered so far. In this work we define a concurrent DEL product, propose a mechanism to resolve conflicts between actions, and define concurrent DEL games. As in the turn-based case, the obtained concurrent infinite game arenas can be finitely represented when all actions are public, or all are propositional. Thus we identify cases where the strategic epistemic logic ATL*K can be model checked on such games.

The global internet of vehicles market is growing rapidly, it is estimated to increase significantly its value by the next few years. Vehicular Ad hoc Networks (VANETs) has a central role in the development of Intelligent Transportation System, since vehicles can communicate with each other. This paper proposes a model integrating both 5G and Blockchain for vehicular ad-hoc network management. This choice is motivated by the need of guaranteeing secure and reliable information exchange between vehicles. 5G provides low latency communication improving both V2V (Vehicle to Vehicle) and V2I (Vehicle to Infrastructure) connections increasing considerably their trustworthiness. On the other side, BlockChain offers a distributed ledger, enhancing security and data reliability. These technologies together with VANETs mechanism can provide multiple new opportunities and uses, such as automating braking system. In this work, not only we provide a complete overview of these technologies, but also we suggest a new research topic, based on the integration of such technologies with VANETs environment, to obtain a very robust network, and hence a safer traffic management.