Visiting Professor Carlos Olarte (ECT-UFRN, Brazil), joint work with Linda Brodo

Abstract:
The Core Network Algebra (CNA) is a model for concurrency that extends the point-to-point communication discipline of Milner?s CCS with multiparty interactions.
Links are used to build chains describing how information flows among the different agents participating in a multiparty interaction. The inherent non-determinism in deciding both, the number of participants in an interaction and how they synchronize, makes it difficult to devise efficient verification techniques for this language. In this talk I will present a symbolic semantics and a symbolic bisimulation for CNA which are more menable for automating reasoning. Unlike the operational semantics of CNA, the symbolic semantics is finitely branching and it represents, compactly, a possibly infinite number of transitions. We give necessary and sufficient conditions to efficiently check the validity of symbolic configurations.
We also propose a smooth extension of the Hennessy-Milner logic to deal with CNA processes and symbolic transitions. Finally, I will present an executable rewriting logic specification of both the symbolic semantics and the modal logic, thus obtaining verification procedures to analyze CNA processes. I will profit this talk to give a gentle introduction to process calculi and CCS.
Hence, no previous knowledge on these topics are required from the audience.

Biography:
Carlos Olarte is CNPq Researcher (Level 2 - Computer Science) and assistant professor at ECT - UFRN (Brazil) since April 2014. Before that, he was associate professor at Pontificia Universidad Javeriana Cali (Colombia). He got his Ph.D. from LIX, École Polytechnique (France) in 2009 under the supervision of Prof. Catuscia Palamidessi and Prof. Frank Valencia. He has worked in declarative models for concurrency where processes can be seen as both, computing agents and formulas in a given logic. These works have found application in the specification and verification of systems in different application domains, e.g., biochemical systems, multimedia interactive systems and security protocols. His complete list of publication is available at sites.google.com/site/carlosolarte/. In 2018, Carlos will be in a sabbatical leave and he will work at TU-Wien in the Computational Logic Group under supervision of Prof. Agata Ciabattoni.