The Library
Leafy automata for higher-order concurrency
Tools
Dixon, Alex, Lazic, Ranko, Murawski, Andrzej S. and Walukiewicz, Igor (2021) Leafy automata for higher-order concurrency. In: FoSSaCS 21 , Virtual conference, 27 Mar-1 Apr 2021. Published in: FOSSACS 2021: Foundations of Software Science and Computation Structures , 12650 pp. 184-204. ISBN 9783030719944. doi:10.1007/978-3-030-71995-1_10
|
PDF
WRAP-Leafy-automata-higher-order-concurrency-2021.pdf - Published Version - Requires a PDF viewer. Available under License Creative Commons Attribution 4.0. Download (492Kb) | Preview |
|
PDF
WRAP-Leafy-automata-higher-order-concurrency-2021.pdf - Accepted Version Embargoed item. Restricted access to Repository staff only - Requires a PDF viewer. Download (344Kb) |
Official URL: https://doi.org/10.1007/978-3-030-71995-1_10
Abstract
Finitary Idealized Concurrent Algol ( FICA ) is a prototypical programming language combining functional, imperative, and concurrent computation. There exists a fully abstract game model of FICA , which in principle can be used to prove equivalence and safety of FICA programs. Unfortunately, the problems are undecidable for the whole language, and only very rudimentary decidable sub-languages are known.
We propose leafy automata as a dedicated automata-theoretic formalism for representing the game semantics of FICA . The automata use an infinite alphabet with a tree structure. We show that the game semantics of any FICA term can be represented by traces of a leafy automaton. Conversely, the traces of any leafy automaton can be represented by a FICA term. Because of the close match with FICA , we view leafy automata as a promising starting point for finding decidable subclasses of the language and, more generally, to provide a new perspective on models of higher-order concurrent computation.
Moreover, we identify a fragment of FICA that is amenable to verification by translation into a particular class of leafy automata. Using a locality property of the latter class, where communication between levels is restricted and every other level is bounded, we show that their emptiness problem is decidable by reduction to Petri net reachability.
Item Type: | Conference Item (Paper) | ||||||
---|---|---|---|---|---|---|---|
Alternative Title: | |||||||
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||||
Library of Congress Subject Headings (LCSH): | ALGOL (Computer program language) , Machine theory, Game theory, Programming languages (Electronic computers) | ||||||
Series Name: | Lecture Notes in Computer Science | ||||||
Journal or Publication Title: | FOSSACS 2021: Foundations of Software Science and Computation Structures | ||||||
Publisher: | Elsevier | ||||||
ISBN: | 9783030719944 | ||||||
Official Date: | 23 March 2021 | ||||||
Dates: |
|
||||||
Volume: | 12650 | ||||||
Page Range: | pp. 184-204 | ||||||
DOI: | 10.1007/978-3-030-71995-1_10 | ||||||
Status: | Peer Reviewed | ||||||
Publication Status: | Published | ||||||
Access rights to Published version: | Open Access (Creative Commons) | ||||||
Date of first compliant deposit: | 25 January 2021 | ||||||
Date of first compliant Open Access: | 2 September 2021 | ||||||
Conference Paper Type: | Paper | ||||||
Title of Event: | FoSSaCS 21 | ||||||
Type of Event: | Conference | ||||||
Location of Event: | Virtual conference | ||||||
Date(s) of Event: | 27 Mar-1 Apr 2021 | ||||||
Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year