Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Workflow Net Fitness Measures ...


view this post on Zulip Email Gateway (Feb 09 2026 at 13:15):

From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>

Dear all,

I’d like to announce a new AFP-entry.

Enjoy,
René

Workflow Net Fitness Measures
by Moritz Manke

Abstract

This entry covers workflow nets, a specialization of Petri nets, which are
especially useful for modelling business processes. It then defines measures for
the fitness of these nets, namely trace fitness and causal footprint fitness.
These attempt to measure how well a model covers all of the traces in an event
log (a multiset of traces, which have happened in the business). Most fitness
measures are far from perfect and a number of attributes have been defined in
literature. The main goal of this entry is to formalize proofs for some of these
attributes of fitness measures and learning how to correctly define the measures
and attributes along the way.

https://www.isa-afp.org/entries/Workflow_Net_Fitness_Measures.html


Last updated: Feb 22 2026 at 05:16 UTC