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.
Project MembersUniversità degli Studi di Cagliari - Dipartimento di Matematica e Informatica
- 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.
- 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.
- 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.
- 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.