We present a method for generating random hypergraphs in context-free hypergraph languages. It is obtained by adapting Mairson's generation algorithm for context-free string grammars to the setting of hyperedge replacement grammars. Our main results are that for non-ambiguous hyperedge replacement grammars, the method generates hypergraphs uniformly at random and in quadratic time. We illustrate our approach by a running example of a hyperedge replacement grammar generating term graphs.
Formal verification methods for concurrent systems cannot always be scaled-down or tailored in order to be applied on specific subsystems. We address such an issue in a MultiParty Session Types setting by devising a partial type assignment system for multiparty sessions (i.e. sets of concurrent participants) with asynchronous communications. Sessions are possibly typed by "asynchronous global types" describing the overall behaviour of specific subsets of participants only (from which the word "partial"). Typability is proven to ensure that sessions enjoy the partial versions of the well-known properties of lock- and orphan-message-freedom.
Interaction nets are a form of restricted graph rewrite system that can serve as a graphical or textual programming language. As such, benefits include one-step confluence, ease of parallelism and explicit garbage collection. However, some of these restrictions burden the programmer, so they have been extended in several ways, notably to include data types and conditional rules. This paper introduces a further extension to allow nested pattern matching and to do so in a way that preserves these benefits and fundamental properties of interaction nets. We also show that by introducing a translation to non-nested matching, this extension is conservative in rewriting. In addition, we propose a new notation to express this pattern matching.
Pnueli first noticed that certain simple 'counting' properties appear to be inexpressible in popular timed temporal logics such as Metric Interval Temporal Logic (MITL). This interesting observation has since been studied extensively, culminating in strong timed logics that are capable of expressing such properties yet remain decidable. A slightly more general case, namely where one asserts the existence of a sequence of events in an arbitrary interval of the form (instead of an upper-bound interval of the form [0, b>, which starts from the current point in time), has however not been addressed satisfactorily in the existing literature. We show that counting in [0, b> is in fact as powerful as counting in ; moreover, the general property 'there exist x', x'' is an element of I such that x' <= x'' and Psi(x', x'') holds' can be expressed in Extended Metric Interval Temporal Logic (EMITL) with only [0, b>.
As a supplement to my talk at the workshop, this extended abstract motivates and summarizes my work with co-authors on problems in two separate areas: first, in the A-calculus with letrec, a universal model of computation, and second, on Milner's process interpretation of regular expressions, a proper subclass of the finite-state processes. The aim of my talk was to motivate a transferal of ideas for workable concepts of structure-constrained graphs: from the problem of finding compact graph representations for terms in the lambda-calculus with letrec to the problem of recognizing finite process graphs that can be expressed by regular expressions. In both cases the construction of structure-constrained graphs was expedient in order to enable to go back and forth easily between, in the first case, lambda-terms and term graphs, and in the second case, regular expressions and process graphs. The main focus here is on providing pointers to my work with co-authors, in both areas separately. A secondary focus is on explaining directions of my present projects, and describing research questions of possibly general interest that have developed out of my work in these two areas.
