Title: Model checking based on Kronecker algebra Author: Peter Kemper and Ralf Luebeck Abstract: Reachability analysis is a general approach to analyze Petri nets, but the state space explosion often permits its application. In the field of performance analysis of stochastic Petri nets, modular representations of reachability graphs using Kronecker algebra have been successfully applied. This paper describes how a Kronecker representation of the reachability graph is employed for exploration of the reachability set and subsequent model checking of ordinary Petri nets and Computational Tree Logic. A new and space efficient representation of the reachability set is given. A non-trivial model of a production cell is exercised to demonstrate the usefulness of the approach. Extensions towards certain colored Petri nets are briefly sketched. Published in: Universität Dortmund, Fachbereich Informatik, Forschungsbericht Nr. 669, 1998