Jesper G. Henriksen
Ole J. L. Jensen
Michael E. Jørgensen
Anders B. Sandholm
In TACAS, pages 58--73
The potential applications are numerous. We discuss text processing, Boolean circuits, and distributed systems. Our main example is an automatic proof of properties for the ``Dining Philosophers with Encyclopedia'' example by Kurshan and MacMillan. We establish these properties for the parameterized case without the use of induction.
Our results show that, contrary to common beliefs, high computational complexity may be a desired feature of a specification formalism.
Aarhus University, Denmark and New York University, USA.
Available as PostScript.