CPN-AMI is a computer-aided software engineering environment based on Petri Net specifications.
[1] It provides the ability to specify the behavior of a distributed system—and to evaluate properties such as invariants (preservation of resources), absence of deadlocks, liveness, or temporal logic properties (relations between events in the system).
CPN-AMI relies on AMI-Nets, that are well-formed Petri nets with syntactic facilities.
This Petri net class supports symbolic techniques for model checking, and thus provides a very compressed way to store all states of a system.
Since 2016 CPN-AMI has been listed by the owners as "still available but not maintained any more" (Lib6/MoVe Software at the Wayback Machine (archived May 5, 2016)).