Download=========IMPORTANT==========
A new version can be found at:
http://countingfluents.weebly.com
This page will be updated soon
=============================
Counting Fluent Linear-Time Temporal Logic (CFLTL) is an extension of Fluent Linear-Time Temporal Logic, which complements the notion of fluent by the related concept of counting fluent. As opposed to the binary nature of fluents (which are logical propositions), counting fluents are numerical values, that enumerate event occurrences, and allow one to specify naturally some properties of reactive systems, such as bounded liveness and other properties in which the number of occurrences of certain events is relevant. CFLTL is an undecidable, strictly more expressive, extension of fluent linear temporal logic. Although a sound (but incomplete) model checking approach for the logic can be used.
Project Samples
