Temporal analysis of λσ activity systems

λσ is a simulation language based on Whitehead´s (1960) theory of reality and formalized in the typed λ-calculus. λσ entities are described as elements of a type and λσ activities are subtypes. Type inference algorithms can be used to analyze and verify models in which the flow of entities is deterministic. In this paper, the authors describe the use of temporal logic to analyze and verify models in which entities move from one activity to another with a given probability. The approach is to apply the proof system for temporal logic with uncertainty of Lehmann and Shelah (1982)