[5-25]Logical characterisations and compositionality of input-output conformance simulation
Title: Logical characterisations and compositionality of input-output conformance simulation
Speaker: Luca Aceto (Reykjavik University, Iceland)
Time: 10:00, Thursday, May 25, 2017
Venue: Room 334, Level 3, Building 5, Institute of Software, Chinese Academy of Sciences (4 Zhongguancun South Fourth Street, Haidian District, Beijing 100190)
Input-output conformance simulation (iocos) has been proposed by Gregorio-Rodríguez, Llana and Martínez-Torres as a simulation-based behavioural preorder underlying model-based testing. This relation is inspired by Tretman's classic ioco relation, but has better worst-case complexity than ioco and supports stepwise refinement.
In this talk, I will develop the theory of iocos by studying logical characterisations of this relation and its compositionality. More specifically, I will present characterisations of iocos in terms of modal logics and compare them with an existing logical characterisation for ioco proposed by Behoar and Mousavi. Moreover, I will discuss ways of defining operations over system descriptions that ensure that the operations preserve iocos and that they take quiescence, namely the absence of system outputs, properly into account.
The talk is based on joint work with Ignacio Fabregas, Carlos Gregorio-Rodriguez and Anna Ingólfsdóttir presented at the 43rd International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2017 available at http://icetcs.ru.is/nosos/sofsem17.pdf.
Luca Aceto is a professor of computer science at Reykjavik University, Iceland, and a member of Academia Europaea (the Academy of Europe). He was president of the European Association for Theoretical Computer Science from July 2012 till July 2016. Before joining Reykjavik University in 2004, he has held permanent academic positions at Aalborg University and the University of Sussex, as well as short-term positions at INRIA Sophia Antipolis and the Hewlett Packard Pisa Science Center.
Luca Aceto's main research interests span concurrency theory (with emphasis on the study of algebraic process description languages and on the techniques they support to specify and reason about reactive systems), logic in computer science, semantics of programming languages, structural operational semantics and its meta-theory, and runtime verification. He has published two books, seven book chapters, 55 journal papers, 65 conference papers, and edited 34 volumes. He has also served as PC chair, organizer of PC member for over 70 conferences and workshops.