Università degli studi di Milano - Bicocca
Dipartimento di Informatica, Sistemistica e Comunicazione (DISCO)
Models of Concurrency,Communication and Computation
We study models and formal techniques for the specification, the analysis and the synthesis of concurrent and distributed systems, considering various aspects of modularity such as compositionality, refinement and abstraction with the aim of preserving behavioural properties. The focus is mainly on general Petri net theory, concurrent automata and the theory of regions, in the framework of the theory of categories.
Hierarchical models of mobile agents are developed as an extension of basic models in Petri net theory, and their application in the framework of bioinspired computational models are investigated.
The algebraic structure of the local states of a Petri net is an orthomodular poset, the algebraic model of quantum logic. The main aim of this research topic is the characterization of the orthomodular posets generated by the state spaces of net systems and the study of the relationships between the axiomatic basis founding net theory and physical theories.
Data types admit circular definitions, therefore share with infinite data structures the same coalgebraic foundations. Syntactical and semantical results on recursive and infinite types exploit this connection, and also the more traditional approach based on the techniques for the solution of recursive domain equations. We have been exploring a systematic treatment of these issues, in the framework of final coalgebras or, dually, of initial iterative algebraic theories.
We are interested in the analysis of circular definitions of "infinite" data structures. Streams, infinite trees or extended natural numbers generally have infinite depth: we study techniques for proving properties of circular definitions and of the objects they define. These use coinduction and the fine structure of final coalgebras with the induced explicit approximation structure on infinite objects.