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