Read out

Guest Talk: Verification techniques for a network algebra

Carlos Olarte

Date/Time: 23.02.2018, 11:00

Loca­tion: D2.2.094


The Core Network Algebra (CNA) is a model for concur­rency that extends the poin­t-­to-­point commu­ni­ca­tion disci­pline of Milner’s CCS with multi­party inter­ac­tions. Links are used to build chains descri­bing how infor­ma­tion flows among the diffe­rent agents parti­ci­pa­ting in a multi­party inter­ac­tion. The inherent non-­de­ter­mi­nism in deci­ding both, the number of parti­ci­pants in an inter­ac­tion and how they synchro­nize, makes it diffi­cult to devise effi­cient veri­fi­ca­tion tech­ni­ques for this language. In this talk I will present a symbolic seman­tics and a symbolic bisi­mu­la­tion for CNA which are more amenable for auto­ma­ting reaso­ning. Unlike the opera­tional seman­tics of CNA, the symbolic seman­tics is fini­tely bran­ching and it repres­ents, compactly, a possibly infi­nite number of tran­si­tions. We give necessary and suffi­cient condi­tions to effi­ci­ently check the vali­dity of symbolic confi­gu­ra­tions. We also propose a smooth exten­sion of the Hennes­sy-­Milner logic to deal with CNA processes and symbolic tran­si­tions. Finally, I will present an execu­table rewri­ting logic speci­fi­ca­tion of both the symbolic seman­tics and the modal logic, thus obtai­ning veri­fi­ca­tion proce­dures to analyze CNA processes. I will profit this talk to give a gentle intro­duc­tion to process calculi and CCS. Hence, no previous know­ledge on these topics are required from the audi­ence.


Carlos Olarte is CNPq Rese­ar­cher (Level 2 - Computer Science) and assis­tant professor at ECT - UFRN (Brazil) since April 2014. Before that, he was asso­ciate professor at Ponti­ficia Univer­sidad Jave­riana Cali (Colombia). He got his Ph.D. from LIX, École Poly­tech­nique (France) in 2009 under the super­vi­sion of Prof. Catu­scia Pala­mi­dessi and Prof. Frank Valencia. He has worked in decla­ra­tive models for concur­rency where processes can be seen as both, compu­ting agents and formulas in a given logic. These works have found appli­ca­tion in the speci­fi­ca­tion and veri­fi­ca­tion of systems in diffe­rent appli­ca­tion domains, e.g., bioche­mical systems, multi­media inter­ac­tive systems and secu­rity proto­cols. His complete list of publi­ca­tion is avail­able at In 2018, Carlos will be in a sabba­tical leave and he will work at TU-Wien in the Compu­ta­tional Logic Group under super­vi­sion of Prof. Agata Ciabat­toni.

Back to overview