Informatik, TU Wien

Verification Techniques for a Network Algebra

Lecture by guest professor Carlos Olarte (ECT - UFRN, Brazil), joint work with Linda Brodo.


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 amenable 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.


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 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.


The lecture series on research talks by the visiting professors of the PhD School can also be credited as an elective course for students of master programs of computer science: TISS