Every autumn semester I need Teaching Assistant (TA) for both courses IMT4123 and IIKG2001 ? If you want to help (and be payed for it), send me an e-mail; and we see if you can join even in the middle of the semester!
Categories
Month: August 2021
Categories
Domain Semirings United
Our short paper “Domain Semirings United” coauthored with Uli Fahrenberg, Georg Struth, and Krzysztof Ziemiánski, was accepted by the journal Acta Cybernetica, but will appear only next year (probably in Vol. 25 Nr. 3). In the meantime you can read the paper on the arXiv.
Abstract:
Domain operations on semirings have been axiomatised in two different ways: by a map from an additively idempotent semiring into a boolean subalgebra of the semiring bounded by the additive and multiplicative unit of the semiring, or by an endofunction on a semiring that induces a distributive lattice bounded by the two units as its image. This note presents classes of semirings where these approaches coincide.
Categories
Posets with Interfaces
After quite some time, we have released a long version of our work on “Posets with Interfaces for Concurrent Kleene Algebra“, co-authored with Uli Fahrenberg, Georg Struth, and Krzysztof Ziemiański, which is now being reviewed for a journal.
Abstract:
We introduce posets with interfaces (iposets) and generalise the serial composition of posets to a new gluing composition of iposets. In partial order semantics of concurrency, this amounts to designate events that continue their execution across components. Alternatively, in terms of decomposing concurrent systems, it allows cutting through some events, whereas serial composition may cut through edges only.
We show that iposets under gluing composition form a category, extending the monoid of posets under serial composition, and a 2-category when enriched with a subsumption order and a suitable parallel composition as a lax tensor. This generalises the interchange monoids used in concurrent Kleene algebra.
We also consider gp-iposets, which are generated from singletons by finitary gluing and parallel compositions. We show that the class includes the series-parallel posets as well as the interval orders, which are also well studied in concurrency theory. Finally, we show that not all posets are gp-iposets, exposing several posets that cannot occur as induced substructures of gp-iposets.
Categories
Sculptures in Concurrency
Logical Methods in Computer Science, the most prestigious journal managed solely by the theoretical computer science community, has published our work on Sculptures in Concurrency, co-authored with Uli Fahrenberg, Christopher A. Trotter, and Krzysztof Ziemiański.
Abstract:
We give a formalization of Pratt’s intuitive sculpting process for higher-dimensional automata (HDA). Intuitively, an HDA is a sculpture if it can be embedded in (i.e., sculpted from) a single higher dimensional cell (hypercube). A first important result of this paper is that not all HDA can be sculpted, exemplified through several natural acyclic HDA, one being the famous “broken box” example of van Glabbeek. Moreover, we show that even the natural operation of unfolding is completely unrelated to sculpting, e.g., there are sculptures whose unfoldings cannot be sculpted. We investigate the expressiveness of sculptures, as a proper subclass of HDA, by showing them to be equivalent to regular ST-structures (an event-based counterpart of HDA) and to (regular) Chu spaces over 3 (in their concurrent interpretation given by Pratt). We believe that our results shed new light on the intuitions behind sculpting as a method of modeling concurrent behavior, showing the precise reaches of its expressiveness. Besides expressiveness, we also develop an algorithm to decide whether an HDA can be sculpted. More importantly, we show that sculptures are equivalent to Euclidean cubical complexes (being the geometrical counterpart of our combinatorial definition), which include the popular PV models used for deadlock detection. This exposes a close connection between geometric and combinatorial models for concurrency which may be of use for both areas.
My work with Bjørnar Luteberget and Koen Claessen (from Chalmers) won the Best Paper Award at the 18th Conference on Formal Methods in Computer-Aided Design (FMCAD), which was held in Texas, USA, in November 2018.
The paper is on automatically verifying capacity specifications against railway designs, and contains an associated tool chain based on SAT solvers and Discrete Event Simulation. The paper was selected from 73 papers that were submitted to FMCAD 2018. This conference is ranked as #1 in Formal Methods on the Google Scholar Metrics.
One main technical contribution of this paper is the introduction of the method that we called “SAT modulo DES” which combines the speed of verification of SAT solvers with the power of Discrete Event Simulation engines for handling complex problems such as train dynamics.
The talk of Bjørnar Luteberget was equally praised and made one of the highlights of the conference. Bjørnar also had a Student Paper and a lightning talk in the respective session, describing our initial work on Synthesis for railway designs.
The verification tools were tested on realistic models as below.
My work with Håkon Normann and Thomas Hildebrandt was published in Elsevier’s Journal of Logical and Algebraic Methods in Programming and became the 5th most downloaded paper of 2016.
The paper is entitled “Declarative event based models of concurrency and refinement in psi-calculi”.
My work with Bjørnar Luteberget and Martin Steffen (from PSY and ConSeRNS groups at UiO) won the Best Paper Award at the 12th International Conference on Integrated Formal Methods, which was held in Reykjavik, Iceland in June 2016. The paper was selected from 99 papers.
The paper is on automatically verifying railway regulations against railway designs, and contains an associated tool that was integrated in the RailComplete railway design engineering tool set.
The talk of Bjørnar Luteberget was equally praised and made one of the highlights of the conference. Other highlights included the talks of Turing laureate Tony Hoare on “Unifying Theories of Concurrency” part of UTP 2016 symposium and the talk of Danish Knight Kim G. Larsen on the amazing verification tool Uppaal part of the PrePost workshop.
A more realistic screenshot from the presented tool.
Scholarship for Fully Funded Student Participant in Marktoberdorf International Summer School on Software System Reliability and Security, hosted by NATO Security Through Science Committee and Institut fur Informatik of Technische Universitat Munchen, Germany, during 1-13 August 2006.
Scholarship for Fully Funded Student Participant in ICCL Summer School on Logic-based Knowledge Representation, at the Technische Universitat Dresden, Germany 2-17 July 2005.