The Beauty of Predicate Automata

Azadeh Farzan; Zachary Kincaid

doi:10.1007/978-3-032-13711-1_4

The Beauty of Predicate Automata

Azadeh Farzan
, Zachary Kincaid

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Chapter

Abstract

In [6], we introduced a class data automata, called Predicate Automata, which recognize languages over an alphabet Σ×N where Σ is a finite alphabet. These automata were designed to capture the behaviour of parametrized programs, i.e. programs with an unbounded number of threads, and their correctness proofs. Since the focus of [6] was on the verification problem, the paper does not investigate the properties of these automata beyond the minimum which is necessary for the verification problem. In this paper, we study some of their key properties and relate them to other classes of data automata.

Original language	English (US)
Title of host publication	Lecture Notes in Computer Science
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	54-74
Number of pages	21
DOIs	https://doi.org/10.1007/978-3-032-13711-1_4
State	Published - 2026

Publication series

Name	Lecture Notes in Computer Science
Volume	14765 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-032-13711-1_4

Cite this

@inbook{bfdd4a02be67412e900ceacb5339e5f0,

title = "The Beauty of Predicate Automata",

abstract = "In [6], we introduced a class data automata, called Predicate Automata, which recognize languages over an alphabet Σ×N where Σ is a finite alphabet. These automata were designed to capture the behaviour of parametrized programs, i.e. programs with an unbounded number of threads, and their correctness proofs. Since the focus of [6] was on the verification problem, the paper does not investigate the properties of these automata beyond the minimum which is necessary for the verification problem. In this paper, we study some of their key properties and relate them to other classes of data automata.",

author = "Azadeh Farzan and Zachary Kincaid",

note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.",

year = "2026",

doi = "10.1007/978-3-032-13711-1\_4",

language = "English (US)",

series = "Lecture Notes in Computer Science",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "54--74",

booktitle = "Lecture Notes in Computer Science",

address = "Germany",

}

TY - CHAP

T1 - The Beauty of Predicate Automata

AU - Farzan, Azadeh

AU - Kincaid, Zachary

PY - 2026

Y1 - 2026

N2 - In [6], we introduced a class data automata, called Predicate Automata, which recognize languages over an alphabet Σ×N where Σ is a finite alphabet. These automata were designed to capture the behaviour of parametrized programs, i.e. programs with an unbounded number of threads, and their correctness proofs. Since the focus of [6] was on the verification problem, the paper does not investigate the properties of these automata beyond the minimum which is necessary for the verification problem. In this paper, we study some of their key properties and relate them to other classes of data automata.

AB - In [6], we introduced a class data automata, called Predicate Automata, which recognize languages over an alphabet Σ×N where Σ is a finite alphabet. These automata were designed to capture the behaviour of parametrized programs, i.e. programs with an unbounded number of threads, and their correctness proofs. Since the focus of [6] was on the verification problem, the paper does not investigate the properties of these automata beyond the minimum which is necessary for the verification problem. In this paper, we study some of their key properties and relate them to other classes of data automata.

UR - https://www.scopus.com/pages/publications/105030921224

UR - https://www.scopus.com/pages/publications/105030921224#tab=citedBy

U2 - 10.1007/978-3-032-13711-1_4

DO - 10.1007/978-3-032-13711-1_4

M3 - Chapter

AN - SCOPUS:105030921224

T3 - Lecture Notes in Computer Science

SP - 54

EP - 74

BT - Lecture Notes in Computer Science

PB - Springer Science and Business Media Deutschland GmbH

ER -