Library probsa.rt.model.rt_monotonic

(* --------------------------------- ProBsa --------------------------------- *)
From probsa.probability Require Export dominance_relation.
From probsa.rt.behavior Require Export response_time.

(* ---------------------------------- Main ---------------------------------- *)

pRT-Monotonicity

In this section, we introduce a notion of response-time monotonic transformation of a system.
Section ProbabilisticResponseTimeMonotonicity.

Assume that horizon defines the termination time of the system. If horizon = None, the system will not terminate. If horizon = Some B, then the system will terminate at time B, and jobs that are not completed by that time will be considered to never have finished.
  Variable horizon : option instant.

Consider a set of jobs ...
  Context {Job : JobType}.

... and any kind of processor state model.
  Context {PState : ProcessorState Job}.

Ground Truth System

Consider a system that is described by a ground truth sample space Ωg and a ground truth probability measure μg.
  Context {Ωg} {μg : measure Ωg}.

Next, consider two parameters -- job_cost and job_arrival.
  Context {job_cost : JobCostRV Job Ωg μg}
          {job_arrival : JobArrivalRV Job Ωg μg}.

Finally, assume we have a schedule of jobs in the ground truth system.
  Variable pr_sched_Ωg : pr_schedule μg PState.

Transformed System

Next, we consider a transformed system with new Ωs, μs, job arrivals, job costs, as well as new schedule pr_sched_Ωs.
  Context {Ωs} {μs : measure Ωs}.
  Context {job_cost_s : JobCostRV Job Ωs μs}
          {job_arrival_s : JobArrivalRV Job Ωs μs}.
  Variable pr_sched_Ωs : pr_schedule μs PState.

Probabilistic Response-Time Monotonicity

System (Ωs, μs) is a result of a response-time monotone transformation of system (Ωg, μg) if the response time of a job j in system (Ωg, μg) is upper-bounded (in the sense of stochastic domination, ⪯) by the response time of j in system (Ωs, μs).
  Definition probabilistic_response_time_monotone_transformation :=
    ∀ j, response_time pr_sched_Ωg horizon j ⪯ response_time pr_sched_Ωs horizon j.

End ProbabilisticResponseTimeMonotonicity.