Opin vandamál í jöfnurökfræði ferla - verkefni lokið
Fréttatilkynning verkefnisstjóra
Computer scientists use programming and specification languages to communicate with machines and with one another. Ideally, each such language should come equipped with “laws of programming” that capture when two expressions describe the same “computational behaviour” and
can therefore be used interchangeably. The “laws of programming” can, for instance, be used to optimize computer programs or to prove mathematically that a computing system behaves as expected.
Equational logic is the branch of mathematics and theoretical computer science that has been used to study whether sufficiently powerful “laws of programming” with some desirable characteristics exist for a plethora of languages. In particular, research on algebraic process description languages has yielded finite collections of laws that can be used to prove all equalities between expressions simply by “replacing equals for equals.” However, despite over forty years of extensive research, the study of “laws of programming” for process description languages still has many foundational unresolved problems.
The overarching goal of this project was to solve some of the challenging open problems in the
equational axiomatization of behavioural equivalences over process calculi and to develop novel
proof techniques for establishing such results. In particular, the project
• obtained a full characterization of the notions of “program equivalence” for which the
equational theory of parallel composition can be finitely described,
• extended classic, negative and positive results on the finite axiomatizability of strong
bisimilarity, the yardstick notion of “program equivalence”, over CCS to the setting of
equivalences abstracting from internal steps in computations, and
• developed general techniques for transferring positive and negative results on the existence
of finite equational axiomatizations of process equivalences between languages.
The results obtained within this project have led to an improved understanding of the power of the classic logic of equations in describing and reasoning about a ubiquitous class of computing systems, and will have impact on future work on algebraic methods in concurrency theory. Moreover, the techniques used to achieve them have expanded the toolbox of the working concurrency theorist and will be applied to specific, unsolved axiomatic questions that still remain tantalisingly open. Moreover, the project will have impact though the doctoral students and postdoctoral researchers who were trained as part of the research work and who have taken up positions at high-class research institutions in Europe.
Information on how the results will be applied:
The results of the project and the proof techniques developed to achieve them have sown the seeds for future research. They will be used in subsequent work by the project team and the concurrency theory community at large.
A list of the project’s outputs:
The list of all the publications, submitted articles and manuscripts that resulted from the project is,and will remain, available on the project’s web site at http://icetcs.ru.is/opel/. Overall, the project produced nine journal papers, 12 conference papers, three book chapters and one PhD thesis. Three articles resulting from the project are under submission for journal publication. All publications are accessible in open access form from the project’s web site. Moreover, seven of the project publications are also available in diamond open access.
Heiti verkefnis: Opin vandamál í jöfnurökfræði ferla/Open Problems
in the Equational Logic of Processes (OPEL)
Verkefnisstjóri: Luca Aceto,
Háskólanum í Reykjavík
Tegund styrks: Verkefnisstyrkur
Styrktímabil: 2019-2021
Fjárhæð styrks kr. 54.525.000
Tilvísunarnúmer Rannís: 196050
