The state space of a transition system is defined as a quotient set (i.e. a set of equivalence classes) of terms of a top most sort State, and the transitions are defined with conditional rewrite rules over the quotient set. A property to be verified is either (1) an …
read moreQuantitative formalisms of regularity, a partial survey
Abstract. The question of extending the concept of regularity to a more quantitative setting has been considered since the origins of formal language theory and a large number of solutions to this question have been proposed. In in this lecture, I will review only a part of them. First, I …
read moreSE4MCP with Reo Part 2
A promising new application domain for coordination languages is programming protocols among threads in multi-core programs: coordination languages typically provide high-level constructs and abstractions that more easily compose into correct---with respect to a programmer's intentions---protocol specifications than do low-level synchronization constructs provided by conventional languages (e.g., locks, semaphores, etc …
read moreA decomposition theorem for finite monoid actions
Groups actions over sets became a powerful tool for the study of the inner structure of groups. The study of basic concepts such as orbit or stabilizer leads to the canonical bijection between the orbits of an action and the corresponding set of cosets of the group. This fundamental result …
read moreSocial Network Simulation Part I: Model Selection for Realistic Social Network Generation
Nowadays, social networks appear in different forms in various domains. Online social networks, mobile communication networks, co-authoring networks and human interactions in real life are some examples of social networks. Today, analysis of dynamics and evolution of social networks is an important field of research. In this area, computer simulation …
read moreCompositional metric reasoning with Probabilistic Process Calculi
Probabilistic process calculi are algebraic theories to specify and verify probabilistic concurrent systems. Bisimulation metric is a fundamental semantic notion that defines the behavioral distance of probabilistic processes. We study which operators of probabilistic process calculi allow for compositional reasoning with respect to bisimulation metric semantics. Moreover, we characterize the …
read moreTowards Practical Verification of Dynamically Typed Programs
Dynamically typed languages enable programmers to write elegant, reusable and extendable programs. Recently, some progress has been made regarding their verification. However, the user is currently required to manually show the absence of type errors, a tedious task usually involving large amounts of repetitive work.
As most dynamically typed programs …
read moreA formalization of bisimulation-up-to techniques and their meta-theory
Bisimilarity of two processes is formally established by producing a bisimulation relation, i.e. a set of pairs of process expressions that contains those two processes and obeys certain closure properties. In many situations, particularly when the underlying labeled transition system is unbounded, these bisimulation relations can be large and …
read moreAutomata learning: a categorical perspective
Automata learning is a known technique to infer a finite state machine from a set of observations. In this paper, we revisit Angluin's original algorithm from a categorical perspective. This abstract view on the main ingredients of the algorithm lays a uniform framework to derive algorithms for other types of …
read moreArden's rule and the Kleene-Schützenberger theorem
We will take a look at a classical result by Schützenberger, generalizing Kleene's theorem to formal power series, and give a proof of this result that closely resembles Rutten's coinductive proof of Kleene's theorem (1998). It turns out that the key ingredient of a proof consists of a combination of …
read more