Showing 1–19 of 19 results for author: Dardha, O

Multiparty Session Types with a Bang!

Authors: Matthew Alan Le Brun, Simon Fowler, Ornela Dardha

Abstract: Replication is an alternative construct to recursion for describing infinite behaviours in the pi-calculus. In this paper we explore the implications of including type-level replication in Multiparty Session Types (MPST), a behavioural type theory for message-passing programs. We introduce MPST!, a session-typed multiparty process calculus with replication and first-class roles. We show that repli… ▽ More Replication is an alternative construct to recursion for describing infinite behaviours in the pi-calculus. In this paper we explore the implications of including type-level replication in Multiparty Session Types (MPST), a behavioural type theory for message-passing programs. We introduce MPST!, a session-typed multiparty process calculus with replication and first-class roles. We show that replication is not an equivalent alternative to recursion in MPST, and that using both replication and recursion in one type system in fact allows us to express both context-free protocols and protocols that support mutual exclusion and races. We demonstrate the expressiveness of MPST! on examples including binary tree serialisation, dining philosophers, and a model of an auction, and explore the implications of replication on the decidability of typechecking. △ Less

Submitted 24 January, 2025; originally announced January 2025.

MAG$π$!: The Role of Replication in Typing Failure-Prone Communication

Authors: Matthew Alan Le Brun, Ornela Dardha

Abstract: MAG$π$ is a Multiparty, Asynchronous and Generalised $π$-calculus that introduces timeouts into session types as a means of reasoning about failure-prone communication. Its type system guarantees that all possible message-loss is handled by timeout branches. In this work, we argue that the previous is unnecessarily strict. We present MAG$π$!, an extension serving as the first introduction of repli… ▽ More MAG$π$ is a Multiparty, Asynchronous and Generalised $π$-calculus that introduces timeouts into session types as a means of reasoning about failure-prone communication. Its type system guarantees that all possible message-loss is handled by timeout branches. In this work, we argue that the previous is unnecessarily strict. We present MAG$π$!, an extension serving as the first introduction of replication into Multiparty Session Types (MPST). Replication is a standard $π$-calculus construct used to model infinitely available servers. We lift this construct to type-level, and show that it simplifies specification of distributed client-server interactions. We prove properties relevant to generalised MPST: subject reduction, session fidelity and process property verification. △ Less

Submitted 24 April, 2024; originally announced April 2024.

Session Types for the Transport Layer: Towards an Implementation of TCP

Authors: Samuel Cavoj, Ivan Nikitin, Colin Perkins, Ornela Dardha

Abstract: Session types are a typing discipline used to formally describe communication-driven applications with the aim of fewer errors and easier debugging later into the life cycle of the software. Protocols at the transport layer such as TCP, UDP, and QUIC underpin most of the communication on the modern Internet and affect billions of end-users. The transport layer has different requirements and constr… ▽ More Session types are a typing discipline used to formally describe communication-driven applications with the aim of fewer errors and easier debugging later into the life cycle of the software. Protocols at the transport layer such as TCP, UDP, and QUIC underpin most of the communication on the modern Internet and affect billions of end-users. The transport layer has different requirements and constraints compared to the application layer resulting in different requirements for verification. Despite this, to our best knowledge, no work shows the application of session types at the transport layer. In this work, we discuss how multiparty session types (MPST) can be applied to implement the TCP protocol. We develop an MPST-based implementation of a subset of a TCP server in Rust and test its interoperability against the Linux TCP stack. Our results highlight the differences in assumptions between session type theory and the way transport layer protocols are usually implemented. This work is the first step towards bringing session types into the transport layer. △ Less

Submitted 8 April, 2024; originally announced April 2024.

Comments: In Proceedings PLACES 2024, arXiv:2404.03712

Journal ref: EPTCS 401, 2024, pp. 22-36

EXPRESSing Session Types

Authors: Ilaria Castellani, Ornela Dardha, Luca Padovani, Davide Sangiorgi

Abstract: To celebrate the 30th edition of EXPRESS and the 20th edition of SOS we overview how session types can be expressed in a type theory for the standard $π$-calculus by means of a suitable encoding. The encoding allows one to reuse results about the $π$-calculus in the context of session-based communications, thus deepening the understanding of sessions and reducing redundancies in their theoretical… ▽ More To celebrate the 30th edition of EXPRESS and the 20th edition of SOS we overview how session types can be expressed in a type theory for the standard $π$-calculus by means of a suitable encoding. The encoding allows one to reuse results about the $π$-calculus in the context of session-based communications, thus deepening the understanding of sessions and reducing redundancies in their theoretical foundations. Perhaps surprisingly, the encoding has practical implications as well, by enabling refined forms of deadlock analysis as well as allowing session type inference by means of a conventional type inference algorithm. △ Less

Submitted 13 September, 2023; originally announced September 2023.

Comments: In Proceedings EXPRESS/SOS2023, arXiv:2309.05788

Journal ref: EPTCS 387, 2023, pp. 8-25

Traced Types for Safe Strategic Rewriting

Authors: Rongxiao Fu, Ornela Dardha, Michel Steuwer

Abstract: Strategy languages enable programmers to compose rewrite rules into strategies and control their application. This is useful in programming languages, e.g., for describing program transformations compositionally, but also in automated theorem proving, where related ideas have been studies with tactics languages. Clearly, not all compositions of rewrites are correct, but how can we assist programme… ▽ More Strategy languages enable programmers to compose rewrite rules into strategies and control their application. This is useful in programming languages, e.g., for describing program transformations compositionally, but also in automated theorem proving, where related ideas have been studies with tactics languages. Clearly, not all compositions of rewrites are correct, but how can we assist programmers in writing correct strategies? In this paper, we present a static type system for strategy languages. We combine a structural type system capturing how rewrite strategies transform the shape of the rewritten syntax with a novel tracing system that keeps track of all possible legal strategy execution paths. Our type system raises warnings when parts of a composition are guaranteed to fail at runtime, and errors when no legal execution for a strategy is possible. We present a formalization of our strategy language and novel tracing type system, and formally prove its type soundness. We present formal results, showing that ill-traced strategies are guaranteed to fail at runtime and that well-traced strategy executions "can't go wrong", meaning that they are guaranteed to have a possible successful execution path. △ Less

Submitted 27 April, 2023; originally announced April 2023.

Structural Subtyping as Parametric Polymorphism

Authors: Wenhao Tang, Daniel Hillerström, James McKinna, Michel Steuwer, Ornela Dardha, Rongxiao Fu, Sam Lindley

Abstract: Structural subtyping and parametric polymorphism provide similar flexibility and reusability to programmers. For example, both features enable the programmer to provide a wider record as an argument to a function that expects a narrower one. However, the means by which they do so differs substantially, and the precise details of the relationship between them exists, at best, as folklore in literat… ▽ More Structural subtyping and parametric polymorphism provide similar flexibility and reusability to programmers. For example, both features enable the programmer to provide a wider record as an argument to a function that expects a narrower one. However, the means by which they do so differs substantially, and the precise details of the relationship between them exists, at best, as folklore in literature. In this paper, we systematically study the relative expressive power of structural subtyping and parametric polymorphism. We focus our investigation on establishing the extent to which parametric polymorphism, in the form of row and presence polymorphism, can encode structural subtyping for variant and record types. We base our study on various Church-style $λ$-calculi extended with records and variants, different forms of structural subtyping, and row and presence polymorphism. We characterise expressiveness by exhibiting compositional translations between calculi. For each translation we prove a type preservation and operational correspondence result. We also prove a number of non-existence results. By imposing restrictions on both source and target types, we reveal further subtleties in the expressiveness landscape, the restrictions enabling otherwise impossible translations to be defined. More specifically, we prove that full subtyping cannot be encoded via polymorphism, but we show that several restricted forms of subtyping can be encoded via particular forms of polymorphism. △ Less

Submitted 11 September, 2023; v1 submitted 17 April, 2023; originally announced April 2023.

Comments: 47 pages, accepted by OOPSLA 2023

MAG$π$: Types for Failure-Prone Communication

Authors: Matthew Alan Le Brun, Ornela Dardha

Abstract: Multiparty Session Types (MPST) are a typing discipline for communication-centric systems, guaranteeing communication safety, deadlock freedom and protocol compliance. Several works have emerged which model failures and introduce fault-tolerance techniques. However, such works often make assumptions on the underlying network, e.g., TCP-based communication where messages are guaranteed to be delive… ▽ More Multiparty Session Types (MPST) are a typing discipline for communication-centric systems, guaranteeing communication safety, deadlock freedom and protocol compliance. Several works have emerged which model failures and introduce fault-tolerance techniques. However, such works often make assumptions on the underlying network, e.g., TCP-based communication where messages are guaranteed to be delivered; or adopt centralised reliable nodes and an ad-hoc notion of reliability; or only address a single kind of failure, such as node crash failures. In this work, we develop MAG$π$ -- a Multiparty, Asynchronous and Generalised $π$-calculus, which is the first language and type system to accommodate in unison: (i) the widest range of non-Byzantine faults, including message loss, delays and reordering; crash failures and link failures; and network partitioning; (ii) a novel and most general notion of reliability, taking into account the viewpoint of each participant in the protocol; (iii) a spectrum of network assumptions from the lowest UDP-based network programming to the TCP-based application level. We prove subject reduction and session fidelity; process properties (deadlock freedom, termination, etc.); failure-handling safety and reliability adherence. △ Less

Submitted 25 January, 2023; originally announced January 2023.

Comments: To be published in ESOP'23

Proceedings Combined 28th International Workshop on Expressiveness in Concurrency and 18th Workshop on Structural Operational Semantics

Authors: Ornela Dardha, Valentina Castiglioni

Abstract: This volume contains the proceedings of EXPRESS/SOS 2021: the Combined 28th International Workshop on Expressiveness in Concurrency and the 18th Workshop on Structural Operational Semantics, which was held online, as an affiliated workshop of CONCUR 2021, the 32nd International Conference on Concurrency Theory. The EXPRESS/SOS workshop series aims at bringing together researchers interested in the… ▽ More This volume contains the proceedings of EXPRESS/SOS 2021: the Combined 28th International Workshop on Expressiveness in Concurrency and the 18th Workshop on Structural Operational Semantics, which was held online, as an affiliated workshop of CONCUR 2021, the 32nd International Conference on Concurrency Theory. The EXPRESS/SOS workshop series aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models. △ Less

Submitted 21 August, 2021; originally announced August 2021.

Journal ref: EPTCS 339, 2021

Papaya: Global Typestate Analysis of Aliased Objects Extended Version

Authors: Mathias Jakobsen, Alice Ravier, Ornela Dardha

Abstract: Typestates are state machines used in object-oriented programming to specify and verify correct order of method calls on an object. To avoid inconsistent object states, typestates enforce linear typing, which eliminates - or at best limits - aliasing. However, aliasing is an important feature in programming, and the state-of-the-art on typestates is too restrictive if we want typestates to be adop… ▽ More Typestates are state machines used in object-oriented programming to specify and verify correct order of method calls on an object. To avoid inconsistent object states, typestates enforce linear typing, which eliminates - or at best limits - aliasing. However, aliasing is an important feature in programming, and the state-of-the-art on typestates is too restrictive if we want typestates to be adopted in real-world software systems. In this paper, we present a type system for an object-oriented language with typestate annotations, which allows for unrestricted aliasing, and as opposed to previous approaches it does not require linearity constraints. The typestate analysis is global and tracks objects throughout the entire program graph, which ensures that well-typed programs conform and complete the declared protocols. We implement our framework in the Scala programming language and illustrate our approach using a running example that shows the interplay between typestates and aliases. △ Less

Submitted 27 July, 2021; originally announced July 2021.

Separating Sessions Smoothly

Authors: Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, J. Garrett Morris

Abstract: This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, to ensure that structural congruence is type preserving. As a consequence we obtain an operational correspondence between HGV… ▽ More This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, to ensure that structural congruence is type preserving. As a consequence we obtain an operational correspondence between HGV and HCP -- a process calculus based on hypersequents and in a propositions-as-types correspondence with classical linear logic (CLL). Our translations from HGV to HCP and vice-versa both preserve and reflect reduction. HGV scales smoothly to support Girard's Mix rule, a crucial ingredient for channel forwarding and exceptions. △ Less

Submitted 11 July, 2023; v1 submitted 19 May, 2021; originally announced May 2021.

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 3 (July 12, 2023) lmcs:9361

Multiparty Session Types for Safe Runtime Adaptation in an Actor Language (Extended version)

Authors: Paul Harvey, Simon Fowler, Ornela Dardha, Simon J. Gay

Abstract: Human fallibility, unpredictable operating environments, and the heterogeneity of hardware devices are driving the need for software to be able to adapt as seen in the Internet of Things or telecommunication networks. Unfortunately, mainstream programming languages do not readily allow a software component to sense and respond to its operating environment, by discovering, replacing, and communicat… ▽ More Human fallibility, unpredictable operating environments, and the heterogeneity of hardware devices are driving the need for software to be able to adapt as seen in the Internet of Things or telecommunication networks. Unfortunately, mainstream programming languages do not readily allow a software component to sense and respond to its operating environment, by discovering, replacing, and communicating with components that are not part of the original system design, while maintaining static correctness guarantees. In particular, if a new component is discovered at runtime, there is no guarantee that its communication behaviour is compatible with existing components. We address this problem by using multiparty session types with explicit connection actions, a type formalism used to model distributed communication protocols. By associating session types with software components, the discovery process can check protocol compatibility and, when required, correctly replace components without jeapordising safety. We present the design and implementation of EnsembleS, the first actor-based language with adaptive features and a static session type system, and apply it to a case study based on an adaptive DNS server. We formalise the type system of EnsembleS and prove the safety of well-typed programs, making essential use of recent advances in non-classical multiparty session types. △ Less

Submitted 14 May, 2021; originally announced May 2021.

Comments: Extended version of paper to appear at ECOOP 2021

Deadlock-Free Session Types in Linear Haskell

Authors: Wen Kokke, Ornela Dardha

Abstract: Priority Sesh is a library for session-typed communication in Linear Haskell which offers strong compile-time correctness guarantees. Priority Sesh offers two deadlock-free APIs for session-typed communication. The first guarantees deadlock freedom by restricting the process structure to trees and forests. It is simple and composeable, but rules out cyclic structures. The second guarantees deadloc… ▽ More Priority Sesh is a library for session-typed communication in Linear Haskell which offers strong compile-time correctness guarantees. Priority Sesh offers two deadlock-free APIs for session-typed communication. The first guarantees deadlock freedom by restricting the process structure to trees and forests. It is simple and composeable, but rules out cyclic structures. The second guarantees deadlock freedom via priorities, which allows the programmer to safely use cyclic structures as well. Our library relies on Linear Haskell to guarantee linearity, which leads to easy-to-write session types and highly idiomatic code, and lets us avoid the complex encodings of linearity in the Haskell type system that made previous libraries difficult to use. △ Less

Submitted 26 March, 2021; originally announced March 2021.

Prioritise the Best Variation

Authors: Wen Kokke, Ornela Dardha

Abstract: Binary session types guarantee communication safety and session fidelity, but alone they cannot rule out deadlocks arising from the interleaving of different sessions. In Classical Processes (CP)$-$a process calculus based on classical linear logic$-$deadlock freedom is guaranteed by combining channel creation and parallel composition under the same logical cut rule. Similarly, in Good Variation (… ▽ More Binary session types guarantee communication safety and session fidelity, but alone they cannot rule out deadlocks arising from the interleaving of different sessions. In Classical Processes (CP)$-$a process calculus based on classical linear logic$-$deadlock freedom is guaranteed by combining channel creation and parallel composition under the same logical cut rule. Similarly, in Good Variation (GV)$-$a linear concurrent $λ$-calculus$-$deadlock freedom is guaranteed by combining channel creation and thread spawning under the same operation, called fork. In both CP and GV, deadlock freedom is achieved at the expense of expressivity, as the only processes allowed are tree-structured. Dardha and Gay define Priority CP (PCP), which allows cyclic-structured processes and restores deadlock freedom by using priorities, in line with Kobayashi and Padovani. Following PCP, we present Priority GV (PGV), a variant of GV which decouples channel creation from thread spawning. Consequently, we type cyclic-structured processes and restore deadlock freedom by using priorities. We show that our type system is sound by proving subject reduction and progress. We define an encoding from PCP to PGV and prove that the encoding preserves typing and is sound and complete with respect to the operational semantics. △ Less

Submitted 15 December, 2023; v1 submitted 26 March, 2021; originally announced March 2021.

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 4 (December 18, 2023) lmcs:8867

Row-Polymorphic Types for Strategic Rewriting

Authors: Rongxiao Fu, Xueying Qin, Ornela Dardha, Michel Steuwer

Abstract: We present a type system for strategy languages that express program transformations as compositions of rewrite rules. Our row-polymorphic type system assists compiler engineers to write correct strategies by statically rejecting non meaningful compositions of rewrites that otherwise would fail during rewriting at runtime. Furthermore, our type system enables reasoning about how rewriting transfor… ▽ More We present a type system for strategy languages that express program transformations as compositions of rewrite rules. Our row-polymorphic type system assists compiler engineers to write correct strategies by statically rejecting non meaningful compositions of rewrites that otherwise would fail during rewriting at runtime. Furthermore, our type system enables reasoning about how rewriting transforms the shape of the computational program. We present a formalization of our language at its type system and demonstrate its practical use for expressing compiler optimization strategies. Our type system builds the foundation for many interesting future applications, including verifying the correctness of program transformations and synthesizing program transformations from specifications encoded as types. △ Less

Submitted 23 March, 2021; originally announced March 2021.

Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics

Authors: Ornela Dardha, Jurriaan Rot

Abstract: This volume contains the proceedings of EXPRESS/SOS 2020: the Combined 27th International Workshop on Expressiveness in Concurrency and the 17th Workshop on Structural Operational Semantics, which was held online, as an affiliated workshop of CONCUR 2020, the 31st International Conference on Concurrency Theory. The EXPRESS/SOS workshop series aims at bringing together researchers interested in th… ▽ More This volume contains the proceedings of EXPRESS/SOS 2020: the Combined 27th International Workshop on Expressiveness in Concurrency and the 17th Workshop on Structural Operational Semantics, which was held online, as an affiliated workshop of CONCUR 2020, the 31st International Conference on Concurrency Theory. The EXPRESS/SOS workshop series aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models. △ Less

Submitted 27 August, 2020; originally announced August 2020.

Journal ref: EPTCS 322, 2020

π with leftovers: a mechanisation in Agda

Authors: Uma Zalakain, Ornela Dardha

Abstract: Linear type systems need to keep track of how programs use their resources. The standard approach is to use context splits specifying how resources are (disjointly) split across subterms. In this approach, context splits redundantly echo information which is already present within subterms. An alternative approach is to use leftover typing, where in addition to the usual (input) usage context, typ… ▽ More Linear type systems need to keep track of how programs use their resources. The standard approach is to use context splits specifying how resources are (disjointly) split across subterms. In this approach, context splits redundantly echo information which is already present within subterms. An alternative approach is to use leftover typing, where in addition to the usual (input) usage context, typing judgments have also an output usage context: the leftovers. In this approach, the leftovers of one typing derivation are fed as input to the next, threading through linear resources while avoiding context splits. We use leftover typing to define a type system for a resource-aware π-calculus, a process algebra used to model concurrent systems. Our type system is parametrised over a set of usage algebras that are general enough to encompass shared types (free to reuse and discard), graded types (use exactly n number of times) and linear types (use exactly once). Linear types are important in the π-calculus: they ensure privacy and safety of communication and avoid race conditions, while graded and shared types allow for more flexible programming. We provide a framing theorem for our type system, generalise the weakening and strengthening theorems to include linear types, and prove subject reduction. Our formalisation is fully mechanised in about 1850 lines of Agda. △ Less

Submitted 3 September, 2021; v1 submitted 8 May, 2020; originally announced May 2020.

Comparing Type Systems for Deadlock Freedom

Authors: Ornela Dardha, Jorge A. Pérez

Abstract: Message-passing software systems exhibit non-trivial forms of concurrency and distribution; they are expected to follow intended protocols among communicating services, but also to never "get stuck". This intuitive requirement has been expressed by liveness properties such as progress or (dead)lock freedom and various type systems ensure these properties for concurrent processes. Unfortunately, ve… ▽ More Message-passing software systems exhibit non-trivial forms of concurrency and distribution; they are expected to follow intended protocols among communicating services, but also to never "get stuck". This intuitive requirement has been expressed by liveness properties such as progress or (dead)lock freedom and various type systems ensure these properties for concurrent processes. Unfortunately, very little is known about the precise relationship between these type systems and the classes of typed processes they induce. This paper puts forward the first comparative study of different type systems for message-passing processes that guarantee deadlock freedom. We compare two classes of deadlock-free typed processes, here denoted L and K. The class L stands out for its canonicity: it results from Curry-Howard interpretations of linear logic propositions as session types. The class K, obtained by encoding session types into Kobayashi's linear types with usages, includes processes not typable in other type systems. We show that L is strictly included in K, and identify the precise conditions under which they coincide. We also provide two type-preserving translations of processes in K into processes in L. △ Less

Submitted 6 September, 2021; v1 submitted 1 October, 2018; originally announced October 2018.

Comments: 39 pages, plus appendices. Extended and revised version of an EXPRESS/SOS'15 paper (https://doi.org/10.4204/EPTCS.190.1)

ACM Class: D.3.1; F.3.2

Comparing Deadlock-Free Session Typed Processes

Authors: Ornela Dardha, Jorge A. Pérez

Abstract: Besides respecting prescribed protocols, communication-centric systems should never "get stuck". This requirement has been expressed by liveness properties such as progress or (dead)lock freedom. Several typing disciplines that ensure these properties for mobile processes have been proposed. Unfortunately, very little is known about the precise relationship between these disciplines--and the class… ▽ More Besides respecting prescribed protocols, communication-centric systems should never "get stuck". This requirement has been expressed by liveness properties such as progress or (dead)lock freedom. Several typing disciplines that ensure these properties for mobile processes have been proposed. Unfortunately, very little is known about the precise relationship between these disciplines--and the classes of typed processes they induce. In this paper, we compare L and K, two classes of deadlock-free, session typed concurrent processes. The class L stands out for its canonicity: it results naturally from interpretations of linear logic propositions as session types. The class K, obtained by encoding session types into Kobayashi's usage types, includes processes not typable in other type systems. We show that L is strictly included in K. We also identify the precise condition under which L and K coincide. One key observation is that the degree of sharing between parallel processes determines a new expressiveness hierarchy for typed processes. We also provide a type-preserving rewriting procedure of processes in K into processes in L. This procedure suggests that, while effective, the degree of sharing is a rather subtle criteria for distinguishing typed processes. △ Less

Submitted 26 August, 2015; originally announced August 2015.

Comments: In Proceedings EXPRESS/SOS 2015, arXiv:1508.06347

ACM Class: F.3.2

Journal ref: EPTCS 190, 2015, pp. 1-15

Recursive Session Types Revisited

Authors: Ornela Dardha

Abstract: Session types model structured communication-based programming. In particular, binary session types for the pi-calculus describe communication between exactly two participants in a distributed scenario. Adding sessions to the pi-calculus means augmenting it with type and term constructs. In a previous paper, we tried to understand to which extent the session constructs are more complex and express… ▽ More Session types model structured communication-based programming. In particular, binary session types for the pi-calculus describe communication between exactly two participants in a distributed scenario. Adding sessions to the pi-calculus means augmenting it with type and term constructs. In a previous paper, we tried to understand to which extent the session constructs are more complex and expressive than the standard pi-calculus constructs. Thus, we presented an encoding of binary session pi-calculus to the standard typed pi-calculus by adopting linear and variant types and the continuation-passing principle. In the present paper, we focus on recursive session types and we present an encoding into recursive linear pi-calculus. This encoding is a conservative extension of the former in that it preserves the results therein obtained. Most importantly, it adopts a new treatment of the duality relation, which in the presence of recursive types has been proven to be quite challenging. △ Less

Submitted 25 August, 2014; originally announced August 2014.

Comments: In Proceedings BEAT 2014, arXiv:1408.5564

Journal ref: EPTCS 162, 2014, pp. 27-34