Opin vísindi

Syntactic approaches to negative results in process algebras and modal logics

Syntactic approaches to negative results in process algebras and modal logics


Title: Syntactic approaches to negative results in process algebras and modal logics
Author: Anastasiadi, Elli   orcid.org/0000-0001-7526-9256
Advisor: Luca Aceto, Anna Ingólfsdóttir
Date: 2022-10-17
Language: English
University/Institute: Reykjavik University
Háskólinn í Reykjavík
School: Tæknisvið (HR)
School of Technology (RU)
Department: Tölvunarfræðideild (HR)
Department of Computer Science (RU)
ISBN: 978-9935-9694-0-8
978-9935-9694-1-5 (eISBN)
Subject: Computer science; Process algebra; Modality (Logic); Linear transition systems; Kripke structures; Concurrency; Negative results; Syntax; Semantics; Equational logic; Computational complexity; Doktorsritgerðir; Tölvunarfræði; Reiknirit; Rökfræði; Merkingarfræði
URI: https://hdl.handle.net/20.500.11815/3683

Show full item record

Abstract:

 
Concurrency as a phenomenon is observed in most of the current computer science trends. However the inherent complexity of analyzing the behavior of such a system is incremented due to the many different models of concurrency, the variety of applications and architectures, as well as the wide spectrum of specification languages and demanded correctness criteria. For the scope of this thesis we focus on state based models of concurrent computation, and on modal logics as specification languages. First we study syntactically the process algebras that describe several different concurrent behaviors, by analyzing their equational theories. Here, we use well-established techniques from the equational logic of processes to older and newer setups, and then transition to the use of more general and novel methods for the syntactical analysis of models of concurrent programs and specification languages. Our main contributions are several positive and negative axiomatizability results over various process algebraic languages and equivalences, along with some complexity results over the satisfiability of multi-agent modal logic with recursion, as a specification language.
 
Samhliða sem fyrirbæri sést í flestum núverandi tölvunarfræði stefnur. Hins vegar er eðlislægt flókið að greina hegðun slíks kerfis- tem er aukið vegna margra mismunandi gerða samhliða, fjölbreytileikans af forritum og arkitektúr, svo og breitt svið forskrifta mælikvarða og kröfðust réttmætisviðmiða. Fyrir umfang þessarar ritgerðar leggjum við áherslu á ástandsbundin líkön af samhliða útreikningum og á formlegum rökfræði sem forskrift tungumálum. Fyrst skoðum við setningafræðilega ferlialgebrurnar sem lýsa nokkrum mismunandi samhliða hegðun, með því að greina jöfnukenningar þeirra. Hér notum við rótgróin tækni mynda jöfnunarrökfræði ferla til eldri og nýrri uppsetningar, og síðan umskipti yfir í notkun almennari og nýrra aðferða fyrir setningafræðileg greining á líkönum samhliða forrita og forskriftartungumála. Helstu framlög okkar eru nokkrar jákvæðar og neikvæðar niðurstöður um axiomatizability yfir ýmis ferli algebrumál og jafngildi, ásamt nokkrum samSveigjanleiki leiðir af því að fullnægjanleiki fjölþátta formrökfræði með endurkomu, sem a forskrift tungumál.
 

Files in this item

This item appears in the following Collection(s)