Amazigh Amrane

Petri nets and higher-dimensional automata

Abstract

Petri nets and their variants are often considered through their interleaved semantics, i.e., considering executions where, at each step, a single transition fires. This is clearly a miss, as Petri nets are a true concurrency model. This paper revisits the semantics of Petri nets as higher-dimensional automata (HDAs) as introduced by van Glabbeek, which methodically take concurrency into account. We extend the translation to include some common features. We consider nets with inhibitor arcs, under both concurrent semantics used in the literature, and generalized self-modifying nets. Finally, we present a tool that implements our translations.

Continue reading

Logic and languages of higher-dimensional automata

Abstract

In this paper we study finite higher-dimensional automata (HDAs) from the logical point of view. Languages of HDAs are sets of finite bounded-width interval pomsets with interfaces (iiPoms$\le k$) closed under order extension. We prove that languages of HDAs are MSO-definable. For the converse, we show that the order extensions of MSO-definable sets of iiPoms$\le k$ are languages of HDAs. Furthermore, both constructions are effective. As a consequence, unlike the case of all pomsets, the order extension of any MSO-definable set of iiPoms$\le k$ is MSO-definable.

Continue reading

Presenting interval pomsets with interfaces

Abstract

Interval-order partially ordered multisets with interfaces (ipomsets) have shown to be a versatile model for executions of concur- rent systems in which both precedence and concurrency need to be taken into account. In this paper, we develop a presentation of ipomsets as generated by a graph of certain discrete ipomsets (starters and terminators) under the relation which composes subsequent starters and subsequent ter- minators. Using this presentation, we show that also subsumptions are generated by elementary relations. We develop a similar correspondence on the automata side, relating higher-dimensional automata, which gen- erate ipomsets, and ST-automata, which generate step sequences, and their respective languages.

Continue reading

Closure and decision properties for higher-dimensional automata

Abstract

Continue reading

Languages of higher-dimensional timed automata

Abstract

We present a new language semantics for real-time concurrency. Its operational models are higher-dimensional timed automata (HDTAs), a generalization of both higher-dimensional automata and timed automata. We define languages of HDTAs as sets of interval-timed pomsets with interfaces. As an application, we show that language inclusion of HDTAs is undecidable. On the other hand, using a region construction we can show that untimings of HDTA languages have enough regularity so that untimed language inclusion is decidable.

Continue reading