A Trusted Reservation Infrastructure for Computational Societies
The goal of this project is to model and develop a trustworthy reservation infrastructure. We are looking for a generic infrastructure, which can be specialized to a wide variety of contexts of reservations: flights, hotels, museums, car pooling, medical examinations, etc.
A key aspect of the project is that the interaction between clients and services should be guided by contracts, which allow clients and services to agree on the required and offered features. Contracts might have, for example, sanctions for the modification or the cancellation of reservations, within agreed time limits. Contracts would be formal entities that would allow, on one side, to establish exactly and without uncertainty the obligations and rights of providers and clients and, on the other side, to formally verify whether or not services respect the advertised contracts. Furthermore, contracts will allow the client to compare different providers of the same service and to choose the most suitable for their desires.
The formal specification of contracts is a main research challenge, since one needs a comprehensive theoretical framework, capable of dealing with all the aspects (deadlines, reputation, sanctions, etc.) needed for modelling all the scenarios of interest.
A further goal of this project is the integration of the reservation infrastructure with social networks. In particular, we aim at developing search and recommendation algorithms to single out the services more suitable to the user needs. Such algorithms will be based both on single user profiling, and on the study of the relation with other users in the community.
This project has been funded by the Autonomous Region of Sardinia, with grant L.R.7/2007-CRP-17285.
Università degli Studi di Cagliari - Dipartimento di Matematica e Informatica
2015
- M. Bartoletti, M. Murgia, A. Scalas, R. Zunino. Verifiable abstractions for contract-oriented systems. Accepted for publication in JLAMP.
- M. Bartoletti, T. Cimoli, M. Murgia, L. Pompianu, A.S. Podda. A contract-oriented middleware. To be presented at FACS 2015.
- M. Bartoletti, R. Zunino. On the decidability of honesty and of its variants. To appear in Proc. WSFM/BEAT, 2015
- M. Bartoletti, I. Castellani, P.M. Deniélou, M. Dezani-Ciancaglini, S. Ghilezan, J. Pantovic, J.A. Pérez, P. Thiemann, B. Toninho, H.T. Vieira. Combining behavioural types with security analysis. Accepted for publication in JLAMP, 2015.
- M. Bartoletti, T. Cimoli, R. Zunino. Compliance in behavioural contracts: a brief survey. Festschrift Symposium in Honour of Pierpaolo Degano, 2015.
- M. Bartoletti, T. Cimoli, G. M. Pinna. Lending Petri nets. Accepted for publication in Science of Computer Programming.
- M. Bartoletti, T. Cimoli, G.M. Pinna, R. Zunino. Contracts as games on event structures. Accepted for publication in JLAMP.
- A. Scalas, M. Bartoletti. The LTS WorkBench. In Proc. ICE, 2015.
- M. Bartoletti, P. Degano, P. Di Giamberardino, R. Zunino. Debits and credits in Petri nets and Linear Logic. In LRC, 2015
- M. Bartoletti, T. Cimoli, M. Murgia, L. Pompianu, A.S. Podda. Compliance and subtyping in timed session types. In Proc. FORTE, 2015.
- M. Bartoletti, T. Cimoli, P. Di Giamberardino, R. Zunino. Vicious circles in contracts and in logic. In Science of Computer Programming 109, 2015.
- M. Bartoletti, J. Lange, A. Scalas, R. Zunino. Choreographies in the wild. In Science of Computer Programming 109, 2015.
- M. Bartoletti, P. Degano, G. Ferrari and R. Zunino. Model checking usage policies. In Mathematical Structures in Computer Science 25(3), 2015.
- M. Bartoletti, T. Cimoli, G.M. Pinna, R. Zunino. Models of circular causality. In Proc. ICDCIT, 2015
- P. Di Giamberardino and U. Dal Lago. On Session Types and Polynomial Time. In Mathematical Structures in Computer Science, 2015.
2014
- M. Bartoletti, T. Cimoli, G. M. Pinna and R. Zunino. Circular causality in event structures. In Fundamenta Informaticae 134(3-4), 2014.
- M. Bartoletti, A. Scalas, R. Zunino. A semantic deconstruction of session types. In Proc. CONCUR, 2014. Longer version with proofs available here
- M. Bartoletti, T. Cimoli, G.M. Pinna. A note on two notions of compliance. In Proc. ICE, 2014.
- M. Bartoletti, M. Murgia, A. Scalas, R. Zunino. Modelling and verifying contract-oriented systems in Maude. In Proc. WRLA, 2014.
- G. Casu, G. M. Pinna. Flow unfolding of multi-clock nets. In Proc. Petri Nets, 2014.
- G. Ciobanu, G.M. Pinna. Catalytic and communicating Petri nets are Turing-complete. Information and Computation, 2014.
2013
- J. Lange and A. Scalas. Choreography synthesis as contract agreement. In Proc. ICE, 2013.
- M. Bartoletti, T. Cimoli, P. Di Giamberardino and R. Zunino. Contract agreements via logic. In Proc. ICE, 2013.
- M. Bartoletti, A. Scalas, E. Tuosto, R. Zunino. Honesty by typing. In Proc. FMOODS-FORTE, 2013.
- M. Bartoletti, T. Cimoli and R. Zunino. A theory of agreements and protection. In Proc. POST, 2013.
- M. Bartoletti, T. Cimoli and G.M. Pinna. Lending Petri nets and contracts. In Proc. FSEN, 2013.
2012
- M. Bartoletti, E. Tuosto, R. Zunino. Contract-oriented Computing in CO2. In Scientific Annals of Computer Science, 22(1), 2012.
- M. Bartoletti, E. Tuosto, R. Zunino. On the realizability of contracts in dishonest systems. In Proc. COORDINATION, 2012.
- M. Bartoletti, T. Cimoli, G.M. Pinna and R. Zunino. An event-based model for contracts. In Proc. PLACES, 2012.
- G. Ciobanu and G.M. Pinna. Catalytic Petri Nets are Turing Complete. In Proc. LATA, 2012.