### Metric Temporal Logic With Counting

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya

February 1, 2016

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Introduction

Metric Temporal Logic is extensively studied Real time Logic in the literature.

Allows timing constraints to be specified along with the temporal ordering.

Exhibits considerable diversity in expressiveness and

decidability properties based on restriction on modalities and type of timing constraints.

In general satisfiability checking for MTL is undecidable. Counting within a given time slot is a very natural and useful property in real time systems.

Thus it becomes interesting to study satisfiability checking for its fragments and their extensions with ability to count.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Introduction

Metric Temporal Logic is extensively studied Real time Logic in the literature.

Allows timing constraints to be specified along with the temporal ordering.

Exhibits considerable diversity in expressiveness and

decidability properties based on restriction on modalities and type of timing constraints.

In general satisfiability checking for MTL is undecidable. Counting within a given time slot is a very natural and useful property in real time systems.

Thus it becomes interesting to study satisfiability checking for its fragments and their extensions with ability to count.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Introduction

Metric Temporal Logic is extensively studied Real time Logic in the literature.

Allows timing constraints to be specified along with the temporal ordering.

Exhibits considerable diversity in expressiveness and

decidability properties based on restriction on modalities and type of timing constraints.

In general satisfiability checking for MTL is undecidable. Counting within a given time slot is a very natural and useful property in real time systems.

Thus it becomes interesting to study satisfiability checking for its fragments and their extensions with ability to count.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Introduction

Metric Temporal Logic is extensively studied Real time Logic in the literature.

Allows timing constraints to be specified along with the temporal ordering.

Exhibits considerable diversity in expressiveness and

decidability properties based on restriction on modalities and type of timing constraints.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Introduction

Metric Temporal Logic is extensively studied Real time Logic in the literature.

Allows timing constraints to be specified along with the temporal ordering.

Exhibits considerable diversity in expressiveness and

decidability properties based on restriction on modalities and type of timing constraints.

In general satisfiability checking for MTL is undecidable.

Counting within a given time slot is a very natural and useful property in real time systems.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Introduction

Metric Temporal Logic is extensively studied Real time Logic in the literature.

Allows timing constraints to be specified along with the temporal ordering.

Exhibits considerable diversity in expressiveness and

decidability properties based on restriction on modalities and type of timing constraints.

In general satisfiability checking for MTL is undecidable.

Counting within a given time slot is a very natural and useful property in real time systems.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Introduction

Metric Temporal Logic is extensively studied Real time Logic in the literature.

Allows timing constraints to be specified along with the temporal ordering.

Exhibits considerable diversity in expressiveness and

decidability properties based on restriction on modalities and type of timing constraints.

In general satisfiability checking for MTL is undecidable.

Counting within a given time slot is a very natural and useful property in real time systems.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Presentation Flow

Model : Timed Words

Timed Logic with Counting : Syntax and Semantics Temporal Projections : Simple and Oversampled Expressiveness Relations with Counting Extensions Satisfiability Checking: Decidability

Conclusion Future Work

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Model : Timed Word

Models over which pointwise MTL Formula is being evaluated .

Finite sequence of symbols along with their corresponding timestamps.In general, timestamps monotonically increases For the purpose of this presentation we will restrict our timed words to be strictly monotonic.

Figure: A finite timed word over Σ ={a,b,c}. A strictly monotonic timed word can be seen as a real line annotated with symbols from Σ

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Model : Timed Word

Models over which pointwise MTL Formula is being evaluated .

Finite sequence of symbols along with their corresponding timestamps.In general, timestamps monotonically increases For the purpose of this presentation we will restrict our timed words to be strictly monotonic.

Figure: A finite timed word over Σ ={a,b,c}. A strictly monotonic timed word can be seen as a real line annotated with symbols from Σ

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Model : Timed Word

Models over which pointwise MTL Formula is being evaluated .

Finite sequence of symbols along with their corresponding timestamps.

In general, timestamps monotonically increases For the purpose of this presentation we will restrict our timed words to be strictly monotonic.

Figure: A finite timed word over Σ ={a,b,c}. A strictly monotonic timed word can be seen as a real line annotated with symbols from Σ

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Model : Timed Word

Models over which pointwise MTL Formula is being evaluated .

Finite sequence of symbols along with their corresponding timestamps.In general, timestamps monotonically increases

For the purpose of this presentation we will restrict our timed words to be strictly monotonic.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Model : Timed Word

Models over which pointwise MTL Formula is being evaluated .

Finite sequence of symbols along with their corresponding timestamps.In general, timestamps monotonically increases For the purpose of this presentation we will restrict our timed words to be strictly monotonic.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Model : Timed Word

Models over which pointwise MTL Formula is being evaluated .

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Presentation Flow

Model : Timed Words

Timed Logic with Counting : Syntax and Semantics Temporal Projections : Simple and Oversampled Expressiveness Relations with Counting Extensions Satisfiability Checking: Decidability

Conclusion Future Work

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Time Logic : Metric Temporal Logic

MTL Syntax

φ ::= AP |φ ∧ φ|φ ∨ φ| ¬φ|φ U_{I} φ|φ S_{I} φ
where I is interval of the formhx,yi,x ∈ N ∪ {0},
y,x∈ N ∪ {0,∞}andh...i ∈ {[...],(...),[...),(...]}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Time Logic : Metric Temporal Logic

MTL Syntax

φ ::= AP |φ ∧ φ|φ ∨ φ| ¬φ|φ U_{I} φ|φ S_{I} φ
whereI is interval of the formhx,yi,x ∈ N ∪ {0},
y,x∈ N ∪ {0,∞}andh...i ∈ {[...],(...),[...),(...]}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Metric Temporal Logic : Semantics

MTL Semantics

ρ,i |= φ1UIφ2 ⇐⇒ ∃j >i ρ,j |=φ2 and τj −τi ∈ I and ∀ i <k <j ρ,k |= φ1

ρ,i |= φ_{1}S_{I}φ_{2} ⇐⇒ ∃j <i ρ,j |=φ_{2} and τ_{i} −τ_{j} ∈
I and ∀ i >k >j ρ,k |= φ1

Ex:

## work-hard U _{[5,10]} giving-up

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Metric Temporal Logic : Semantics

MTL Semantics

ρ,i |= φ1UIφ2 ⇐⇒ ∃j >i ρ,j |=φ2 and τj −τi ∈ I and ∀ i <k <j ρ,k |= φ1

ρ,i |= φ_{1}S_{I}φ_{2} ⇐⇒ ∃j <i ρ,j |=φ_{2} and τ_{i} −τ_{j} ∈
I and ∀ i >k >j ρ,k |= φ1

Ex:

## work-hard U _{[5,10]} giving-up

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Metric Temporal Logic : Semantics

MTL Semantics

ρ,i |= φ1UIφ2 ⇐⇒ ∃j >i ρ,j |=φ2 and τj −τi ∈ I and ∀ i <k <j ρ,k |= φ1

ρ,i |= φ_{1}S_{I}φ_{2} ⇐⇒ ∃j <i ρ,j |=φ_{2} and τ_{i} −τ_{j} ∈
I and ∀ i >k >j ρ,k |= φ1

Ex:

## work-hard U _{[5,10]} giving-up

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Metric Temporal Logic : Semantics

MTL Semantics

ρ,i |= φ1UIφ2 ⇐⇒ ∃j >i ρ,j |=φ2 and τj −τi ∈ I and ∀ i <k <j ρ,k |= φ1

ρ,i |= φ_{1}S_{I}φ_{2} ⇐⇒ ∃j <i ρ,j |=φ_{2} and τ_{i} −τ_{j} ∈
I and ∀ i >k >j ρ,k |= φ1

Ex:

## work-hard U _{[5,10]} giving-up

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Metric Temporal Logic : Semantics

MTL Semantics

ρ,i |= φ1UIφ2 ⇐⇒ ∃j >i ρ,j |=φ2 and τj −τi ∈ I and ∀ i <k <j ρ,k |= φ1

ρ,i |= φ_{1}S_{I}φ_{2} ⇐⇒ ∃j <i ρ,j |=φ_{2} and τ_{i} −τ_{j} ∈
I and ∀ i >k >j ρ,k |= φ1

Ex:

## work-hard U _{[5,10]} giving-up

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Time Logic : MTL Fragments

Subclasses:

By restricting set of allowed intervals. e.g. MTL[Unp,Snp], where np refers to non-punctual intervals. It is well known as MITL in the literature.

By restricting set of operators. We denote MTL[W] for
subclass of MTL restricted to operators inW. e.g. MTL[ U_{I}]
where only until operator is allowed.

We will restrict to future only fragment of MTL.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Time Logic : MTL Fragments

Subclasses:

By restricting set of allowed intervals. e.g. MTL[Unp,Snp], wherenp refers to non-punctual intervals. It is well known as MITL in the literature.

By restricting set of operators. We denote MTL[W] for
subclass of MTL restricted to operators inW. e.g. MTL[ U_{I}]
where only until operator is allowed.

We will restrict to future only fragment of MTL.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Time Logic : MTL Fragments

Subclasses:

By restricting set of allowed intervals. e.g. MTL[Unp,Snp], wherenp refers to non-punctual intervals. It is well known as MITL in the literature.

By restricting set of operators. We denote MTL[W] for subclass of MTL restricted to operators inW. e.g. MTL[ UI] where only until operator is allowed.

We will restrict to future only fragment of MTL.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Time Logic : MTL Fragments

Subclasses:

By restricting set of allowed intervals. e.g. MTL[Unp,Snp], wherenp refers to non-punctual intervals. It is well known as MITL in the literature.

By restricting set of operators. We denote MTL[W] for subclass of MTL restricted to operators inW. e.g. MTL[ UI] where only until operator is allowed.

We will restrict to future only fragment of MTL.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Time Logic with counting: CTMTL

We introduce two new modal operators for counting C and UT.

CTMTL Syntax

φ ::= AP |φ ∧ φ|φ ∨ φ| ¬ φ|φ UI,#φ∼n φ|C^{n}_{I}φ
where I is interval of the formhx,yi,x ∈ N ∪ {0},

y,x∈ N ∪ {0,∞},

h...i ∈ {[...],(...),[...),(...]},

∼={≥,≤} and n ∈ N ∪ {0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Time Logic with counting: CTMTL

We introduce two new modal operators for counting C and UT.

CTMTL Syntax

φ ::= AP |φ ∧ φ|φ ∨ φ| ¬ φ|φ UI,#φ∼n φ|C^{n}_{I}φ
whereI is interval of the formhx,yi,x ∈ N ∪ {0},

y,x∈ N ∪ {0,∞},

h...i ∈ {[...],(...),[...),(...]},

∼={≥,≤} and n ∈ N ∪ {0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Time Logic with counting: CTMTL

We introduce two new modal operators for counting C and UT.

CTMTL Syntax

φ ::= AP |φ ∧ φ|φ ∨ φ| ¬ φ|φ UI,#φ∼n φ|C^{n}_{I}φ
whereI is interval of the formhx,yi,x ∈ N ∪ {0},

y,x∈ N ∪ {0,∞},

h...i ∈ {[...],(...),[...),(...]},

∼={≥,≤} and

n ∈ N ∪ {0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Time Logic with counting: CTMTL

We introduce two new modal operators for counting C and UT.

CTMTL Syntax

φ ::= AP |φ ∧ φ|φ ∨ φ| ¬ φ|φ UI,#φ∼n φ|C^{n}_{I}φ
whereI is interval of the formhx,yi,x ∈ N ∪ {0},

y,x∈ N ∪ {0,∞},

h...i ∈ {[...],(...),[...),(...]},

∼={≥,≤} and n ∈ N ∪ {0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### CTMTL: Semantics

ρ,i |= C_{hl}^{∼n}_{,ui}φ ⇐⇒ N_{φ}(hτ_{i} +l, τ_{i} +ui)∼n

ρ,i |= φ1UI,#η∼nφ2 ⇐⇒ ∃j >i ρ,j |=φ2∧τj −τi ∈
I ∧ ∀ ∧i <k <j ρ,k |=φ_{1}∧ N^{0}_{φ}(i,j)∼n

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### CTMTL: Semantics

ρ,i |= C_{hl}^{∼n}_{,ui}φ ⇐⇒ N_{φ}(hτ_{i} +l, τ_{i} +ui)∼n

ρ,i |= φ1UI,#η∼nφ2 ⇐⇒ ∃j >i ρ,j |=φ2∧τj −τi ∈
I ∧ ∀ ∧i <k <j ρ,k |=φ_{1}∧ N^{0}_{φ}(i,j)∼n

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### CTMTL: Semantics

ρ,i |= C_{hl}^{∼n}_{,ui}φ ⇐⇒ N_{φ}(hτ_{i} +l, τ_{i} +ui)∼n

ρ,i |= φ1UI,#η∼nφ2 ⇐⇒ ∃j >i ρ,j |=φ2∧τj −τi ∈
I ∧ ∀ ∧i <k <j ρ,k |=φ_{1}∧ N^{0}_{φ}(i,j)∼n

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Subclasses of CTMTL

C_{(0,1)}MTL: Counting of the formC_{(0,1)}^{∼n} .

C_{(0,u)}MTL: Counting of the formC_{(0,u)}^{∼n} .
CMTL: Counting with C modality only.
TMTL: Counting with UT Modality only.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Subclasses of CTMTL

C_{(0,1)}MTL: Counting of the formC_{(0,1)}^{∼n} .
C_{(0,u)}MTL: Counting of the formC_{(0,u)}^{∼n} .

CMTL: Counting with C modality only. TMTL: Counting with UT Modality only.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Subclasses of CTMTL

C_{(0,1)}MTL: Counting of the formC_{(0,1)}^{∼n} .
C_{(0,u)}MTL: Counting of the formC_{(0,u)}^{∼n} .
CMTL: Counting with C modality only.

TMTL: Counting with UT Modality only.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Subclasses of CTMTL

C_{(0,1)}MTL: Counting of the formC_{(0,1)}^{∼n} .
C_{(0,u)}MTL: Counting of the formC_{(0,u)}^{∼n} .
CMTL: Counting with C modality only.

TMTL: Counting with UT Modality only.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Scheduling HVAC in Demand Response: An Example

In Demand Response system an important requirement is to reduce the Peak Power Demand.

Scheduling of HVAC to limit peak power demand below threshold.

HVAC are more flexible as compared to devices like microwave oven.

Constant mode switching (OFF-¿ON) causes wear and tear and more power consumption due to transient currents. No. of Switch yet another important parameter to grade such scheduling algorithms.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Scheduling HVAC in Demand Response: An Example

In Demand Response system an important requirement is to reduce the Peak Power Demand.

Scheduling of HVAC to limit peak power demand below threshold.

HVAC are more flexible as compared to devices like microwave oven.

Constant mode switching (OFF-¿ON) causes wear and tear and more power consumption due to transient currents.

No. of Switch yet another important parameter to grade such scheduling algorithms.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Scheduling HVAC in Demand Response: An Example

Temperature

24 25 26 27 28 29 30

Time

0 2 4 6 8 10

26.5 Upper Bound

24.5 Lower Bound

AC1 AC2 AC3

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Scheduling HVAC in Demand Response: An Example

♦(0,3),#Switch−ON−AC≤3(Comfort−AC_{1}∧Comfort−AC_{2}∧
Comfort−AC3)

Temperature

24 25 26 27 28 29 30

Time

0 2 4 6 8 10

26.5 Upper Bound

24.5 Lower Bound

AC1 AC2 AC3

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Presentation Flow

Model : Timed Words

Timed Logic with Counting : Syntax and Semantics Temporal Projections : Simple and Oversampled Expressiveness Relations with Counting Extensions Decidability : Satisfiability Checking

Conclusion Future Work

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Definitions: Simple Projection

Let Σ,X be finite disjoint set.

Simple Extension A (Σ,X)-simple extension is a timed word
ρ over 2^{X} ∪Σ such that at any point i ∈dom(ρ),σ_{i}∩Σ6=∅
Simple ProjectionA timed word ρ over Σ obtained by
deleting symbols inX from (Σ,X) extensionρ^{0} is called its
Simple Projection.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Definitions: Simple Projection

Let Σ,X be finite disjoint set.

Simple Extension A (Σ,X)-simple extension is a timed word
ρ over 2^{X} ∪Σ such that at any point i ∈dom(ρ),σ_{i}∩Σ6=∅
Simple ProjectionA timed word ρ over Σ obtained by
deleting symbols inX from (Σ,X) extensionρ^{0} is called its
Simple Projection.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Definitions: Simple Projection

Let Σ,X be finite disjoint set.

Simple Extension A (Σ,X)-simple extension is a timed word
ρ over 2^{X} ∪Σ such that at any point i ∈dom(ρ),σ_{i} ∩Σ6=∅

Simple ProjectionA timed word ρ over Σ obtained by
deleting symbols inX from (Σ,X) extensionρ^{0} is called its
Simple Projection.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Definitions: Simple Projection

Let Σ,X be finite disjoint set.

Simple Extension A (Σ,X)-simple extension is a timed word
ρ over 2^{X} ∪Σ such that at any point i ∈dom(ρ),σ_{i} ∩Σ6=∅
Simple ProjectionA timed word ρ over Σ obtained by
deleting symbols inX from (Σ,X) extensionρ^{0} is called its
Simple Projection.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Definitions: Simple Projection

Let Σ,X be finite disjoint set.

^{X} ∪Σ such that at any point i ∈dom(ρ),σ_{i} ∩Σ6=∅
Simple ProjectionA timed word ρ over Σ obtained by
deleting symbols inX from (Σ,X) extensionρ^{0} is called its
Simple Projection.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Definitions: Simple Projection

Let Σ,X be finite disjoint set.

^{X} ∪Σ such that at any point i ∈dom(ρ),σ_{i} ∩Σ6=∅
Simple ProjectionA timed word ρ over Σ obtained by
deleting symbols inX from (Σ,X) extensionρ^{0} is called its
Simple Projection.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Definitions: Oversampled Projection

Let Σ,X be finite disjoint set.

Oversampled Behaviour A (Σ,X)-oversampled behaviour is
a timed word over 2^{X} ∪Σ, such thatσ_{1}^{0} ∩Σ6=∅ and

σ^{0}_{|dom(ρ}0)|∩Σ6=∅.

Oversampled ProjectionA timed wordρ over Σ obtained by deleting symbols inX (and thus deleting the points

containing only X)from (Σ,X) oversampled behaviour ρ^{0} is
called its Oversampled Projection.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Definitions: Oversampled Projection

Let Σ,X be finite disjoint set.

Oversampled Behaviour A (Σ,X)-oversampled behaviour is
a timed word over 2^{X} ∪Σ, such thatσ_{1}^{0} ∩Σ6=∅ and

σ^{0}_{|dom(ρ}0)|∩Σ6=∅.

Oversampled ProjectionA timed wordρ over Σ obtained by deleting symbols inX (and thus deleting the points

containing only X)from (Σ,X) oversampled behaviour ρ^{0} is
called its Oversampled Projection.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Definitions: Oversampled Projection

Let Σ,X be finite disjoint set.

Oversampled Behaviour A (Σ,X)-oversampled behaviour is
a timed word over 2^{X} ∪Σ, such thatσ_{1}^{0} ∩Σ6=∅ and

σ^{0}_{|dom(ρ}0)|∩Σ6=∅.

Oversampled ProjectionA timed wordρ over Σ obtained by deleting symbols inX (and thus deleting the points

containing only X)from (Σ,X) oversampled behaviour ρ^{0} is
called its Oversampled Projection.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Definitions: Oversampled Projection

Let Σ,X be finite disjoint set.

^{X} ∪Σ, such thatσ_{1}^{0} ∩Σ6=∅ and

σ^{0}_{|dom(ρ}0)|∩Σ6=∅.

containing only X)from (Σ,X) oversampled behaviour ρ^{0} is
called its Oversampled Projection.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Definitions: Oversampled Projection

Let Σ,X be finite disjoint set.

^{X} ∪Σ, such thatσ_{1}^{0} ∩Σ6=∅ and

σ^{0}_{|dom(ρ}0)|∩Σ6=∅.

containing only X)from (Σ,X) oversampled behaviour ρ^{0} is
called its Oversampled Projection.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Definitions: Oversampled Projection

Let Σ,X be finite disjoint set.

^{X} ∪Σ, such thatσ_{1}^{0} ∩Σ6=∅ and

σ^{0}_{|dom(ρ}0)|∩Σ6=∅.

containing only X)from (Σ,X) oversampled behaviour ρ^{0} is
called its Oversampled Projection.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Definitions: Equisaitisfiability modulo Temporal Projection

We say thatϕover Σ is equisatisfiable modulo temporal projection
ψover Σ∪2^{X} iff:

Figure: Figure Illustratingϕis equisatisfiable toψ. Arrow represents the temporal(simple or oversampled) projection function

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Flattening: An example

Flattening is a technique to reduce the modal depth of the formula preserving satisfiability.

Example Let φ=aU_{[2,5]}(bU_{[2,3]}c)

φ_{flat} =aU_{[2,5]}d ∧(d ↔(bU_{[2,3]}c))∧(d →a∨b∨c)

Thus flattening is an example of a reduction preserving satisfiability modulo simple projections.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Flattening: An example

Flattening is a technique to reduce the modal depth of the formula preserving satisfiability.

Example Let φ=aU_{[2,5]}(bU_{[2,3]}c)

φ_{flat} =aU_{[2,5]}d ∧(d ↔(bU_{[2,3]}c))∧(d →a∨b∨c)

Thus flattening is an example of a reduction preserving satisfiability modulo simple projections.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Flattening: An example

Flattening is a technique to reduce the modal depth of the formula preserving satisfiability.

Example Let φ=aU_{[2,5]}(bU_{[2,3]}c)

φ_{flat} =aU_{[2,5]}d ∧(d ↔(bU_{[2,3]}c))∧(d →a∨b∨c)

Thus flattening is an example of a reduction preserving satisfiability modulo simple projections.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Flattening: An example

Flattening is a technique to reduce the modal depth of the formula preserving satisfiability.

Example Let φ=aU_{[2,5]}(bU_{[2,3]}c)

φ_{flat} =aU_{[2,5]}d ∧(d ↔(bU_{[2,3]}c))∧(d →a∨b∨c)

Thus flattening is an example of a reduction preserving satisfiability modulo simple projections.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Flattening: An example

Flattening is a technique to reduce the modal depth of the formula preserving satisfiability.

Example Let φ=aU_{[2,5]}(bU_{[2,3]}c)

φ_{flat} =aU_{[2,5]}d ∧(d ↔(bU_{[2,3]}c))∧(d →a∨b∨c)

Thus flattening is an example of a reduction preserving satisfiability modulo simple projections.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Flattening: An example

Flattening is a technique to reduce the modal depth of the formula preserving satisfiability.

Example Let φ=aU_{[2,5]}(bU_{[2,3]}c)

φ_{flat} =aU_{[2,5]}d ∧(d ↔(bU_{[2,3]}c))∧(d →a∨b∨c)

Thus flattening is an example of a reduction preserving satisfiability modulo simple projections.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Flattening: An example

Flattening is a technique to reduce the modal depth of the formula preserving satisfiability.

Example Let φ=aU_{[2,5]}(bU_{[2,3]}c)

φ_{flat} =aU_{[2,5]}d ∧(d ↔(bU_{[2,3]}c))∧(d →a∨b∨c)

Thus flattening is an example of a reduction preserving satisfiability modulo simple projections.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Related Work

Satisfiability Checking of MITLis decidable with EXPSPACE complexity. [Aluret al.J.ACM 1996]

Satisfiability problem for MTL[ U_{I}] is decidable by reducing it
to reachability problem for 1-clock Timed Alternating

Automata.[Ouaknine et al.LICS 2005]

Satisfiability Checking of QTL with counting is decidable with EXPSPACE complexity. [Rabinovichet.al.FORMATS 2008] Counting adds expressiveness to MITL over signals

[Rabinovich FORMATS 2008].

MTL with counting over signals is expressively complete with FO[<,+1] over reals [HunterCSL 2013].

Counting LTL is equivalent to LTL and has EXP−SPACE complete satisfiability checking.[Laroussinie et.al.TIME 2010].

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Related Work

Satisfiability Checking of MITLis decidable with EXPSPACE complexity. [Aluret al.J.ACM 1996]

Satisfiability problem for MTL[ U_{I}] is decidable by reducing it
to reachability problem for 1-clock Timed Alternating

Automata.[Ouaknine et al.LICS 2005]

Satisfiability Checking of QTL with counting is decidable with EXPSPACE complexity. [Rabinovichet.al.FORMATS 2008] Counting adds expressiveness to MITL over signals

[Rabinovich FORMATS 2008].

MTL with counting over signals is expressively complete with FO[<,+1] over reals [HunterCSL 2013].

Counting LTL is equivalent to LTL and has EXP−SPACE complete satisfiability checking.[Laroussinie et.al.TIME 2010].

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Related Work

Satisfiability Checking of MITLis decidable with EXPSPACE complexity. [Aluret al.J.ACM 1996]

Satisfiability problem for MTL[ U_{I}] is decidable by reducing it
to reachability problem for 1-clock Timed Alternating

Automata.[Ouaknine et al.LICS 2005]

Satisfiability Checking of QTL with counting is decidable with EXPSPACE complexity. [Rabinovichet.al.FORMATS 2008] Counting adds expressiveness to MITL over signals

[Rabinovich FORMATS 2008].

MTL with counting over signals is expressively complete with FO[<,+1] over reals [HunterCSL 2013].

Counting LTL is equivalent to LTL and has EXP−SPACE complete satisfiability checking.[Laroussinie et.al.TIME 2010].

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Related Work

Satisfiability Checking of MITLis decidable with EXPSPACE complexity. [Aluret al.J.ACM 1996]

_{I}] is decidable by reducing it
to reachability problem for 1-clock Timed Alternating

Automata.[Ouaknine et al.LICS 2005]

Satisfiability Checking of QTL with counting is decidable with EXPSPACE complexity. [Rabinovichet.al.FORMATS 2008]

Counting adds expressiveness to MITL over signals [Rabinovich FORMATS 2008].

MTL with counting over signals is expressively complete with FO[<,+1] over reals [HunterCSL 2013].

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Related Work

Satisfiability Checking of MITLis decidable with EXPSPACE complexity. [Aluret al.J.ACM 1996]

_{I}] is decidable by reducing it
to reachability problem for 1-clock Timed Alternating

Automata.[Ouaknine et al.LICS 2005]

Satisfiability Checking of QTL with counting is decidable with EXPSPACE complexity. [Rabinovichet.al.FORMATS 2008]

Counting adds expressiveness to MITL over signals [Rabinovich FORMATS 2008].

MTL with counting over signals is expressively complete with FO[<,+1] over reals [HunterCSL 2013].

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Related Work

Satisfiability Checking of MITLis decidable with EXPSPACE complexity. [Aluret al.J.ACM 1996]

_{I}] is decidable by reducing it
to reachability problem for 1-clock Timed Alternating

Automata.[Ouaknine et al.LICS 2005]

Satisfiability Checking of QTL with counting is decidable with EXPSPACE complexity. [Rabinovichet.al.FORMATS 2008]

Counting adds expressiveness to MITL over signals [Rabinovich FORMATS 2008].

MTL with counting over signals is expressively complete with FO[<,+1] over reals [HunterCSL 2013].

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Related Work

Satisfiability Checking of MITLis decidable with EXPSPACE complexity. [Aluret al.J.ACM 1996]

_{I}] is decidable by reducing it
to reachability problem for 1-clock Timed Alternating

Automata.[Ouaknine et al.LICS 2005]

Counting adds expressiveness to MITL over signals [Rabinovich FORMATS 2008].

MTL with counting over signals is expressively complete with FO[<,+1] over reals [HunterCSL 2013].

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Our Results

Satisfiability Checking for CTMTL is decidable.

Exploring Expressiveness relations amongst fragments of MTL with counting over timed words(Pointwise Semantics).

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Our Results

Satisfiability Checking for CTMTL is decidable.

Exploring Expressiveness relations amongst fragments of MTL with counting over timed words(Pointwise Semantics).

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Our Results

Satisfiability Checking for CTMTL is decidable.

Exploring Expressiveness relations amongst fragments of MTL with counting over timed words(Pointwise Semantics).

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Presentation Flow

Model : Timed Words

Timed Logic with Counting : Syntax and Semantics Temporal Projections : Simple and Oversampled Expressiveness Relations with Counting Extensions Satisfiability Checking: Decidability

Discussion Future Work

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Expressiveness Heirarchy : Logic with counting

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Expressiveness Heirarchy : Non-Punctual Fragments

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### TMTL − CMTL 6= ∅

ϕ=♦_{(0,1),#a≥3}b

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Presentation Flow

Model : Timed Words

Discussion Future Work

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Satisfiability Checking : Decidability

Flatten the formula

All the counting modalities are of the form (w ↔C^{∼n}_{I} a) and
(w ↔aUI,#x∼nb)

Next we eliminate counting modalities from the above flattened formula preserving satisfiability to show decidability.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Satisfiability Checking : Decidability

Flatten the formula

All the counting modalities are of the form (w ↔C^{∼n}_{I} a) and
(w ↔aUI,#x∼nb)

Next we eliminate counting modalities from the above flattened formula preserving satisfiability to show decidability.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Satisfiability Checking : Decidability

Flatten the formula

All the counting modalities are of the form (w ↔C^{∼n}_{I} a) and
(w ↔aUI,#x∼nb)

Next we eliminate counting modalities from the above flattened formula preserving satisfiability to show decidability.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Satisfiability Checking : Decidability

Flatten the formula

All the counting modalities are of the form (w ↔C^{∼n}_{I} a) and
(w ↔aUI,#x∼nb)

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Eliminating C

^{≥n}

_{I}

### b modality

Given a wordρ over Σ we construct a simple extensionρ^{0} over
Σ∪ {b_{0},b_{1}, . . . ,bn−1}

{b_{0},b1, . . . ,bn−1} works as a counter. Using their behaviour
we precisely mark aas the witness for C^{≥n}_{I} b.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Eliminating C

^{≥n}

_{I}

### b modality

Given a wordρ over Σ we construct a simple extensionρ^{0} over
Σ∪ {b_{0},b_{1}, . . . ,bn−1}

{b_{0},b1, . . . ,bn−1} works as a counter. Using their behaviour
we precisely mark aas the witness for C^{≥n}_{I} b.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Eliminating C

^{≥n}

_{I}

### b modality

Given a wordρ over Σ we construct a simple extensionρ^{0} over
Σ∪ {b_{0},b_{1}, . . . ,bn−1}

{b_{0},b1, . . . ,bn−1} works as a counter. Using their behaviour
we precisely mark aas the witness for C^{≥n}_{I} b.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Eliminating UT modality

Given a word ρ over Σ we construct a oversampling ρ^{0} over
Σ∪C ∪B

C ={c0, . . . ,cu}:These propositions oversample the model at

integer time stamps. B=Su

i=0B^{i} where B^{i}={b_{0}^{i}, . . .b^{i}_{n}}: These propositions are
used as counters forb. CounterB^{i} resets at integer point
markedci and saturates once the value reachesntill the next
reset.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Eliminating UT modality

Given a word ρ over Σ we construct a oversampling ρ^{0} over
Σ∪C ∪B

C ={c0, . . . ,cu}:These propositions oversample the model at

integer time stamps. B=Su

i=0B^{i} where B^{i}={b_{0}^{i}, . . .b^{i}_{n}}: These propositions are
used as counters forb. CounterB^{i} resets at integer point
markedci and saturates once the value reachesntill the next
reset.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Eliminating UT modality

Given a word ρ over Σ we construct a oversampling ρ^{0} over
Σ∪C ∪B

C={c0, . . . ,cu}:

These propositions oversample the model at integer time stamps.

B=Su

i=0B^{i} where B^{i}={b_{0}^{i}, . . .b^{i}_{n}}: These propositions are
used as counters forb. CounterB^{i} resets at integer point
markedci and saturates once the value reachesntill the next
reset.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Eliminating UT modality

Given a word ρ over Σ we construct a oversampling ρ^{0} over
Σ∪C ∪B

C={c0, . . . ,cu}:These propositions oversample the model at

integer time stamps.

B=Su

^{i} where B^{i}={b_{0}^{i}, . . .b^{i}_{n}}: These propositions are
used as counters forb. CounterB^{i} resets at integer point
markedci and saturates once the value reachesntill the next
reset.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Eliminating UT modality

Given a word ρ over Σ we construct a oversampling ρ^{0} over
Σ∪C ∪B

C={c0, . . . ,cu}:These propositions oversample the model at

integer time stamps.

B=Su

^{i} where B^{i}={b_{0}^{i}, . . .b^{i}_{n}}: These propositions are
used as counters forb. CounterB^{i} resets at integer point
markedci and saturates once the value reachesntill the next
reset.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Construction of ρ

^{0}

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Marking Witness for UT sub-formula

We count the number of occurrence ofb in two stages:

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Marking Witness for UT sub-formula

We count the number of occurrence ofb in two stages:

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Marking Witness for UT sub-formula

We count the number of occurrence ofb in two stages:

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Marking Witness for UT sub-formula

We count the number of occurrence ofb in two stages:

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Marking Witness for UT sub-formula

Either
n_{1} ≥n∨n_{2} ≥n Or, n_{1}<n∧n_{2}<n and thus bounded number of

cases (disjunctions).

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Marking Witness for UT sub-formula

Either
n_{1} ≥n∨n_{2} ≥n

Or, n_{1}<n∧n_{2}<n and thus bounded number of
cases (disjunctions).

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Marking Witness for UT sub-formula

Either
n_{1} ≥n∨n_{2} ≥n Or, n_{1} <n∧n_{2}<n and thus bounded number of

cases (disjunctions).

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Presentation Flow

Model : Timed Words

Conclusion Future Work

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting

### Conclusion

Two ways of extending MTL with counting threshold constraints is studied.

Both ways add expressiveness to MTL orthogonally. Satisfiability checking for the logic CTMTL is decidable. Both the extensions enjoy benefits of relaxing punctuality. Unlike continuous semantics, pointwise semantics creates a zoo of sub-logics in the expressiveness hierarchy.

S.N.Krishna,Khushraj Madnani, Paritosh.K.Pandya Metric Temporal Logic With Counting