Amazigh Amrane

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