# 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
C^{a 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

- Dixon C, Konev B, Fisher M and Nietiadi S

*Deductive Temporal Reasoning with Constraints*

Journal of Applied Logic, 11(1): 30-51,
Elsevier, 2013

- Dixon C, Fisher M and Konev B,

*Taming the Complexity of Temporal Epistemic Reasoning. *

In: Ghilardi S and Sebastiani R ed(s)
Proceeding of the Seventh International Symposium on the Frontiers of
Combining Systems (FRoCoS'09).
16-18th September, Trento, Italy.
LNAI, Springer 2009

- Dixon, C., Fisher, M., Konev, B., and Lisitsa, A.,

* Practical First-Order Temporal Reasoning*

in the Proceedings of TIME 2008, 16th-18th June 2008,
Montreal, Canada. IEEE Press.

- Dixon, C., Fisher, M., and Konev, B.,

*Temporal Logic with Capacity Constraints*

in the Proceedings of the 6th International Symposium on Frontiers of
Combining Systems (FroCoS), September 10-12, Liverpool, UK.
LNAI, Springer 2007.

- Dixon, C., Fisher, M., and Konev, B.,

*Tractable Temporal Reasoning*

in the Proceedings of the Twentieth International Joint
Conference on Artificial Intelligence (IJCAI-07), pages 318-323, January
6-12th 2007, Hyderabad, India

- Dixon, C., Fisher, M., and Konev, B.,

*Is There a Future for Deductive Temporal Verification?
*

in the Proceedings of TIME 2006, 15th-17th June 2006,
Budapest, Hungary IEEE.

The extended version is published as
University of Liverpool Technical Report number ULMS-06-01

## 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

- Football Specification
- Viable Teams
- Goal Keeper
- Unviable Teams

### Cache Coherence Protocol

- Cache Coherence Protocol Specification for 6 Processes (satisfiable)
- Cache Coherence Protocol for 6 Processes: Non Co-Occurrence for s
and m (unsatisfiable)
- Cache Coherence Protocol for 6 Processes: At most one process can
be in state m (unsatisfiable)

### Dining Philosospher Petri Nets

- Four Person Dining Philosospher Petri Net Specification (satisfiable)
- Four Person Dining Philosospher Petri Net conjoined with
infinitely often every Philospher eats (satisfiable)
- Four Person Dining Philosospher Petri Net conjoined with
sometime Philosphers one and two eat at the same time (unsatisfiable)

### Randomly generated formulae with Overlaps