Safety, Precisely: Quasi-Multidimensional Dyck Languages and a Kleene Theorem

The multiparty session types methodology is used to ensure safe communication between processes (i.e., every send should match a receive, in that order), but is conservative (and thus not complete) in the set of languages it considers as safe. To increase its expressiveness, we generalise the well-known Dyck languages (balanced parentheses, representing sends and receives) such that different types of parentheses can be arbitrarily interleaved instead of the usual hierarchical nesting, resulting in a class of context-sensitive languages, which we call quasi-multidimensional Dyck languages. Focusing on regular subsets of these languages, we give precise syntactic constraints on regular expressions and finite automata which are met iff they represent such a subset. Finally, we extend regular expressions with the multi-ary shuffle on trajectories operator (Mateescu et al.) to obtain what we call safe regular expressions, which we show to precisely represent the aforementioned regular subsets of quasi-multidimensional Dyck languages, allowing for type safety enforced directly through the grammar and thus for safety by construction.  

hosted by