TY - JOUR

T1 - Stratified guarded first-order transition systems

AU - Müller, Christian

AU - Seidl, Helmut

N1 - Publisher Copyright:
© 2022, The Author(s).

PY - 2022

Y1 - 2022

N2 - First-order transition systems are a convenient formalism to specify parametric systems such as multi-agent workflows or distributed algorithms. In general, any nontrivial question about such systems is undecidable. Here, we present three subclasses of first-order transition systems where every universal invariant can effectively be decided via fixpoint iteration. These subclasses are defined in terms of syntactical restrictions: negation, stratification and guardedness. While guardedness represents a particular pattern how input predicates control existential quantifiers, stratification limits the information flow between predicates. Guardedness implies that the weakest precondition for every universal invariant is again universal, while the remaining sufficient criteria enforce that either the number of occurring negated literals decreases in every iteration, or the number of required instances of input predicates or the number of first-order variables remains bounded. We argue for each of these three cases that termination of the fixpoint iteration can be guaranteed. We apply these results to identify classes of multi-agent systems, when formalized as first-order transition systems, where noninterference in presence of declassification is decidable for coalitions of attackers of bounded size.

AB - First-order transition systems are a convenient formalism to specify parametric systems such as multi-agent workflows or distributed algorithms. In general, any nontrivial question about such systems is undecidable. Here, we present three subclasses of first-order transition systems where every universal invariant can effectively be decided via fixpoint iteration. These subclasses are defined in terms of syntactical restrictions: negation, stratification and guardedness. While guardedness represents a particular pattern how input predicates control existential quantifiers, stratification limits the information flow between predicates. Guardedness implies that the weakest precondition for every universal invariant is again universal, while the remaining sufficient criteria enforce that either the number of occurring negated literals decreases in every iteration, or the number of required instances of input predicates or the number of first-order variables remains bounded. We argue for each of these three cases that termination of the fixpoint iteration can be guaranteed. We apply these results to identify classes of multi-agent systems, when formalized as first-order transition systems, where noninterference in presence of declassification is decidable for coalitions of attackers of bounded size.

KW - Decidability

KW - First-order transition systems

KW - Multi-agent systems

KW - Noninterference

KW - Universal invariants

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

U2 - 10.1007/s10703-022-00404-9

DO - 10.1007/s10703-022-00404-9

M3 - Article

AN - SCOPUS:85142413935

SN - 0925-9856

JO - Formal Methods in System Design

JF - Formal Methods in System Design

ER -