Temporal Logic with Cardinality Constraints


Temporal Logic with Cardinality Constraints

Temporal Logic with Cardinality Constraints (TLC) is propositional linear time temporal logic (PTL) with some additional constraints, which restrict the numbers of literals that can be satisfied at any moment in time. TLC is parameterised by (not necessarily disjoint) sets Ca m where a is either = or <= and m is a Natural Number.

A special case of this (termed TLX) is where exactly one literal in each set is true at any moment.

People

With Clare Dixon, Michael Fisher, Boris Konev, Alexei Lisitsa, Sherly Nietiadi, and Wentao Zhen.

Publications

Software

The prover for the logic outlined in the paper Temporal Logic with Capacity Constraints, and fully described in the paper Deductive Temporal Reasoning with Constraints has been implemented in the prover BeTL. Currently BeTL is being re-written but please email us if you are interested in a copy of the new version when it becomes available.

Sample Files

The example files from the draft paper Deductive Temporal Reasoning with Constraints can be found below.

Football Teams

Cache Coherence Protocol

Dining Philosospher Petri Nets

Randomly generated formulae with Overlaps