---
id: 20251223163648
title: Deterministic Parity Automata
type: permanent
created: 2025-12-23T21:36:48Z
modified: 2025-12-23T21:40:09Z
tags: []
---

# Deterministic Parity Automata

Deterministic parity automata are a type of automata where
the environment and the system play against one another, and
describes the interactions therein. DPA are exhaustive, and
end up with a result determining which player 'wins'. 

DPA's have a scoring mechanism that results in an even or
odd final score. An even final score indicates that the
'controller' wins the game. There is no input from the
environment that can't be controlled by the controller. All
traces end up in a favorable state, with no infinite loops.
An odd score means the opposite. There exists some limit
cycle where the controller can't reach a desired mode and
stay there. 

DPA's are used in [[strix]]. They're how Strix does it's
generation from temporal logics to a final automaton.