# A Logic for Non-Deterministic Parallel Abstract State Machines

## TL;DR

This paper introduces a logic for reasoning about single steps of non-deterministic parallel Abstract State Machines, enabling formal analysis of their behavior while maintaining logical completeness.

## Contribution

It extends existing hierarchical ASM logic to handle non-determinism without losing completeness for step-based reasoning.

## Key findings

- Logic effectively models bounded and unbounded non-determinism
- Maintains completeness for invariants and rule equivalence
- Enables formal verification of non-deterministic parallel ASMs

## Abstract

We develop a logic which enables reasoning about single steps of non-deterministic parallel Abstract State Machines (ASMs). Our logic builds upon the unifying logic introduced by Nanchen and St\"ark for reasoning about hierarchical (parallel) ASMs. Our main contribution to this regard is the handling of non-determinism (both bounded and unbounded) within the logical formalism. Moreover, we do this without sacrificing the completeness of the logic for statements about single steps of non-deterministic parallel ASMs, such as invariants of rules, consistency conditions for rules, or step-by-step equivalence of rules.