Formal Construction of Probability Space on Concurrent Systems
Yusen Zhang · Computer Engineering and Science · 2008
The paper describes concurrent systems with Paulson's inductive approach.In the paper,a set of generation sets is given,which is suitable for defining measures.The relation between the measure of finite executions and the measure of the sets of infinite runs is evaluated with a canonical function.It is proved that the measure of the sets of infinite runs is positive and countably additive.With the Caratheodory's extension theorem,the probability space on the set of infinite runs of concurrent systems is constructed.All scripts are checked with Isabell/HOL/Isar.