On the specification of higher dimensional automata

Richard Buckland, Michael Johnson, Dominic Verity

Research output: Contribution to journalArticleResearchpeer-review

Abstract

Higher dimensional automata (HDA) have been widely studied as models of concurrent processes. Most current work focuses on developing the directed algebraic topological notions required to analyse HDA to determine their computer scientific properties (deadlock, safety, unreachable states, etc). Instead, this paper is concerned with the software engineering of HDA and details the specification of HDA by process algebra operations. The specifications work for cubical HDA, but are designed to also work for the explicit choice higher dimensional automata (ECHDA) originally proposed by Buckland. We introduce ω-multigraphs, a graphical notion which is easier to use than pasting schemes but more general than cubical complexes, we describe basic process algebra operations on ECHDA as constructions on ω-multigraphs, we discuss the trichotomy of concurrent, conferring, and conflicting choices, and note that the "deadlock choice" can arise from intersecting conflicting choices, and we remark that common software engineering refinements correspond to choice refinement.

LanguageEnglish
Pages3-13
Number of pages11
JournalElectronic Notes in Theoretical Computer Science
Volume68
Issue number1
DOIs
Publication statusPublished - Nov 2002

Fingerprint

Algebra
Automata
Software engineering
High-dimensional
Specification
Specifications
Process Algebra
Multigraph
Deadlock
Software Engineering
Concurrent
Refinement
Cubical Complex
Basic Algebra
Safety

Cite this

@article{567cce6bdb2247b78a2e1218a5b90619,
title = "On the specification of higher dimensional automata",
abstract = "Higher dimensional automata (HDA) have been widely studied as models of concurrent processes. Most current work focuses on developing the directed algebraic topological notions required to analyse HDA to determine their computer scientific properties (deadlock, safety, unreachable states, etc). Instead, this paper is concerned with the software engineering of HDA and details the specification of HDA by process algebra operations. The specifications work for cubical HDA, but are designed to also work for the explicit choice higher dimensional automata (ECHDA) originally proposed by Buckland. We introduce ω-multigraphs, a graphical notion which is easier to use than pasting schemes but more general than cubical complexes, we describe basic process algebra operations on ECHDA as constructions on ω-multigraphs, we discuss the trichotomy of concurrent, conferring, and conflicting choices, and note that the {"}deadlock choice{"} can arise from intersecting conflicting choices, and we remark that common software engineering refinements correspond to choice refinement.",
author = "Richard Buckland and Michael Johnson and Dominic Verity",
year = "2002",
month = "11",
doi = "10.1016/S1571-0661(04)80497-3",
language = "English",
volume = "68",
pages = "3--13",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "1",

}

On the specification of higher dimensional automata. / Buckland, Richard; Johnson, Michael; Verity, Dominic.

In: Electronic Notes in Theoretical Computer Science, Vol. 68, No. 1, 11.2002, p. 3-13.

Research output: Contribution to journalArticleResearchpeer-review

TY - JOUR

T1 - On the specification of higher dimensional automata

AU - Buckland, Richard

AU - Johnson, Michael

AU - Verity, Dominic

PY - 2002/11

Y1 - 2002/11

N2 - Higher dimensional automata (HDA) have been widely studied as models of concurrent processes. Most current work focuses on developing the directed algebraic topological notions required to analyse HDA to determine their computer scientific properties (deadlock, safety, unreachable states, etc). Instead, this paper is concerned with the software engineering of HDA and details the specification of HDA by process algebra operations. The specifications work for cubical HDA, but are designed to also work for the explicit choice higher dimensional automata (ECHDA) originally proposed by Buckland. We introduce ω-multigraphs, a graphical notion which is easier to use than pasting schemes but more general than cubical complexes, we describe basic process algebra operations on ECHDA as constructions on ω-multigraphs, we discuss the trichotomy of concurrent, conferring, and conflicting choices, and note that the "deadlock choice" can arise from intersecting conflicting choices, and we remark that common software engineering refinements correspond to choice refinement.

AB - Higher dimensional automata (HDA) have been widely studied as models of concurrent processes. Most current work focuses on developing the directed algebraic topological notions required to analyse HDA to determine their computer scientific properties (deadlock, safety, unreachable states, etc). Instead, this paper is concerned with the software engineering of HDA and details the specification of HDA by process algebra operations. The specifications work for cubical HDA, but are designed to also work for the explicit choice higher dimensional automata (ECHDA) originally proposed by Buckland. We introduce ω-multigraphs, a graphical notion which is easier to use than pasting schemes but more general than cubical complexes, we describe basic process algebra operations on ECHDA as constructions on ω-multigraphs, we discuss the trichotomy of concurrent, conferring, and conflicting choices, and note that the "deadlock choice" can arise from intersecting conflicting choices, and we remark that common software engineering refinements correspond to choice refinement.

UR - http://www.scopus.com/inward/record.url?scp=15844396559&partnerID=8YFLogxK

U2 - 10.1016/S1571-0661(04)80497-3

DO - 10.1016/S1571-0661(04)80497-3

M3 - Article

VL - 68

SP - 3

EP - 13

JO - Electronic Notes in Theoretical Computer Science

T2 - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 1

ER -