diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/core/abstract_rta.v
index 0bc2fd8d4663ca69d72c1f8fe82c35efa2c8614e..cab1b614c6fe128b865e8eff5e1997c1856ca69e 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_rta.v
@@ -1,5 +1,5 @@
 From rt.util Require Import tactics nat sum ssromega.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Import job task preemption.preemption_model.
 From rt.restructuring.analysis Require Import schedulability ideal_schedule.
 From rt.restructuring.analysis.abstract Require Import run_to_completion_threshold. 
diff --git a/restructuring/analysis/abstract/core/abstract_seq_rta.v b/restructuring/analysis/abstract/core/abstract_seq_rta.v
index 1f028a88d2456f4a68298dc324f0ad35252d1596..08d40389f42ac1cd1feec4288d3a3dc7d4f6f87e 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_seq_rta.v
@@ -1,5 +1,5 @@
 From rt.util Require Import epsilon tactics rewrite_facilities sum counting list.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Import service.
 From rt.restructuring.model Require Import job task preemption.preemption_model.
 From rt.restructuring.model.arrival Require Import arrival_curves. 
 From rt.restructuring.model.schedule Require Import sequential.
@@ -241,7 +241,7 @@ Section Sequential_Abstract_RTA.
       Proof. 
         move => JA; move: (H_j2_from_tsk) => /eqP TSK2eq.
         move: (posnP (@job_cost _ H3 j2)) => [ZERO|POS].
-        { by rewrite /completed_by /schedule.completed_by ZERO. }    
+        { by rewrite /completed_by /service.completed_by ZERO. }    
         move: (H_interference_and_workload_consistent_with_sequential_jobs
                  j1 t1 t2 H_j1_arrives H_j1_from_tsk H_j1_cost_positive H_busy_interval) => SWEQ.
         eapply all_jobs_have_completed_equiv_workload_eq_service
@@ -336,7 +336,7 @@ Section Sequential_Abstract_RTA.
               rewrite /cumul_task_interference /definitions.cumul_interference
                       /Sequential_Abstract_RTA.cumul_task_interference /task_interference_received_before
                       /task_scheduled_at /task_schedule.task_scheduled_at /service_of_jobs_at
-                      /service_of_jobs.service_of_jobs_at /scheduled_at /schedule.scheduled_at /scheduled_in;
+                      /service_of_jobs.service_of_jobs_at /scheduled_at /service.scheduled_at /scheduled_in;
                 simpl.
               rewrite !H_idle.
               rewrite big1_eq addn0 add0n. 
@@ -369,7 +369,7 @@ Section Sequential_Abstract_RTA.
               rewrite /cumul_task_interference /definitions.cumul_interference
                       /Sequential_Abstract_RTA.cumul_task_interference /task_interference_received_before
                       /task_scheduled_at /task_schedule.task_scheduled_at /service_of_jobs_at
-                      /service_of_jobs.service_of_jobs_at /scheduled_at /schedule.scheduled_at /scheduled_in; simpl.
+                      /service_of_jobs.service_of_jobs_at /scheduled_at /service.scheduled_at /scheduled_in; simpl.
               have ARRs: arrives_in arr_seq j'; first by apply H_jobs_come_from_arrival_sequence with t; apply/eqP.
               rewrite H_sched H_not_job_of_tsk; simpl.
               rewrite (negbTE (option_inj_neq (neqprop_to_neqbool
@@ -410,7 +410,7 @@ Section Sequential_Abstract_RTA.
               rewrite /cumul_task_interference /definitions.cumul_interference
                       /Sequential_Abstract_RTA.cumul_task_interference /task_interference_received_before
                       /task_scheduled_at /task_schedule.task_scheduled_at /service_of_jobs_at
-                      /service_of_jobs.service_of_jobs_at /scheduled_at /schedule.scheduled_at /scheduled_in; simpl.
+                      /service_of_jobs.service_of_jobs_at /scheduled_at /service.scheduled_at /scheduled_in; simpl.
               have ARRs: arrives_in arr_seq j'; first by apply H_jobs_come_from_arrival_sequence with t; apply/eqP.
               rewrite H_sched H_not_job_of_tsk addn0; simpl;
                 rewrite [Some j' == Some j](negbTE (option_inj_neq (neq_sym H_j_neq_j'))) addn0.
@@ -419,7 +419,7 @@ Section Sequential_Abstract_RTA.
                 { by move: H_t_in_interval => /andP [NEQ1 NEQ2]; apply/andP; split; last apply ltn_trans with (t1 + x). }
                 move: (H_work_conserving j t1 t2 t H_j_arrives H_job_of_tsk H_job_cost_positive H_busy_interval NEQT) => [Hn _].
                 apply/eqP;rewrite eq_sym eqb_id; apply/negPn/negP; intros CONTR; move: CONTR => /negP CONTR.
-                apply Hn in CONTR; rewrite /schedule.scheduled_at in CONTR; simpl in CONTR.
+                apply Hn in CONTR; rewrite /service.scheduled_at in CONTR; simpl in CONTR.
                   by rewrite H_sched [Some j' == Some j](negbTE (option_inj_neq (neq_sym H_j_neq_j'))) in CONTR.
               }
               rewrite big_mkcond; apply/sum_seq_gt0P; exists j'; split; last first.
@@ -469,14 +469,14 @@ Section Sequential_Abstract_RTA.
               rewrite /cumul_task_interference /definitions.cumul_interference
                       /Sequential_Abstract_RTA.cumul_task_interference /task_interference_received_before
                       /task_scheduled_at /task_schedule.task_scheduled_at /service_of_jobs_at
-                      /service_of_jobs.service_of_jobs_at /scheduled_at /schedule.scheduled_at /scheduled_in.
+                      /service_of_jobs.service_of_jobs_at /scheduled_at /service.scheduled_at /scheduled_in.
               rewrite H_sched H_job_of_tsk neq_antirefl addn0; simpl.
               move: (H_work_conserving j _ _ t H_j_arrives H_job_of_tsk H_job_cost_positive H_busy_interval) => WORK.
               feed WORK.
               { move: H_t_in_interval => /andP [NEQ1 NEQ2].
                   by apply/andP; split; last apply ltn_trans with (t1 + x). }
               move: WORK => [_ ZIJT].
-              feed ZIJT; first by rewrite /schedule.scheduled_at /scheduled_at H_sched; simpl.
+              feed ZIJT; first by rewrite /service.scheduled_at /scheduled_at H_sched; simpl.
               move: ZIJT => /negP /eqP; rewrite eqb_negLR; simpl; move => /eqP ZIJT; rewrite ZIJT; simpl; rewrite add0n.
               rewrite !eq_refl; simpl; rewrite big_mkcond //=; apply/sum_seq_gt0P.
                 by exists j; split; [apply j_is_in_arrivals_between | rewrite /job_of_task H_job_of_tsk H_sched !eq_refl]. 
@@ -696,7 +696,7 @@ Section Sequential_Abstract_RTA.
         move: (posnP (@job_cost _ H3 j)) => [ZERO|POS].
         { exfalso.
           move: COMPL => /negP COMPL; apply: COMPL.
-            by rewrite /schedule.completed_by /completed_by ZERO.
+            by rewrite /service.completed_by /completed_by ZERO.
         }            
         set (A := job_arrival j - t1) in *.
         apply leq_trans with
diff --git a/restructuring/analysis/abstract/core/definitions.v b/restructuring/analysis/abstract/core/definitions.v
index 125492f692e4798dd07dfe3d6f9b20c751b1a41a..56e6d79bebf4ca910c14d7f023b520e79ecabc45 100644
--- a/restructuring/analysis/abstract/core/definitions.v
+++ b/restructuring/analysis/abstract/core/definitions.v
@@ -1,5 +1,5 @@
 From rt.util Require Import all.
-From rt.restructuring.behavior Require Import job schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Import task processor.ideal.
   
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
diff --git a/restructuring/analysis/abstract/core/run_to_completion_threshold.v b/restructuring/analysis/abstract/core/run_to_completion_threshold.v
index b25bf326b91b2c9fd7d71fc6329ae5e202bf3b9a..3df959fd19444805f380e6d80ae7d09e4e45f268 100644
--- a/restructuring/analysis/abstract/core/run_to_completion_threshold.v
+++ b/restructuring/analysis/abstract/core/run_to_completion_threshold.v
@@ -1,5 +1,5 @@
 From rt.util Require Import epsilon sum tactics search_arg.
-From rt.restructuring.behavior Require Import job schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.analysis.basic_facts Require Import completion.
 From rt.restructuring.model Require Import job task preemption.preemption_model.
 
diff --git a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v b/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
index bf2f724f0e5070070cd8451a9d464e317ef09d62..bf6fa2b342977cd56901b4cdb93c8d632d283024 100644
--- a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
+++ b/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
@@ -1,5 +1,5 @@
 From rt.util Require Import nat sum tactics.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Import job task preemption.preemption_model.
 From rt.restructuring.analysis Require Import service completion ideal_schedule.
 From rt.restructuring.analysis.abstract Require Import run_to_completion_threshold core.definitions.
diff --git a/restructuring/analysis/arrival/rbf.v b/restructuring/analysis/arrival/rbf.v
index cb9b771409ac8ab4654148b59d971e28fd067bce..6159f10d3064651f182ce6e9a9f64f6aa7a89583 100644
--- a/restructuring/analysis/arrival/rbf.v
+++ b/restructuring/analysis/arrival/rbf.v
@@ -1,5 +1,5 @@
 From rt.util Require Import all.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Import job task.
 From rt.restructuring.model.aggregate Require Import task_arrivals.
 From rt.restructuring.model.arrival Require Import arrival_curves.
diff --git a/restructuring/analysis/arrival/workload_bound.v b/restructuring/analysis/arrival/workload_bound.v
index 91688c0b406ba89c8ff454f83f5b5ca2668e6bf0..11d998ccee1332e5d97d1db5c932444b1366fe97 100644
--- a/restructuring/analysis/arrival/workload_bound.v
+++ b/restructuring/analysis/arrival/workload_bound.v
@@ -1,5 +1,5 @@
 From rt.util Require Import sum.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Import task schedule.priority_based.priorities.
 From rt.restructuring.model.aggregate Require Import task_arrivals.
 From rt.restructuring.model.arrival Require Import arrival_curves.
diff --git a/restructuring/analysis/basic_facts/arrivals.v b/restructuring/analysis/basic_facts/arrivals.v
index 75602ba60a8c62fd79e991b60742af937ca65f0e..361c73159fcc1d9fa2872e852f5755f976208f52 100644
--- a/restructuring/analysis/basic_facts/arrivals.v
+++ b/restructuring/analysis/basic_facts/arrivals.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export arrival_sequence schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.util Require Import all.
 
 (* In this section, we relate job readiness to [has_arrived]. *)
diff --git a/restructuring/analysis/basic_facts/completion.v b/restructuring/analysis/basic_facts/completion.v
index 582c4d82953880b8f5aa9efa5a74fe140e3028fc..4263486dd97836b340e41508eed68dcfa518b0a9 100644
--- a/restructuring/analysis/basic_facts/completion.v
+++ b/restructuring/analysis/basic_facts/completion.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.analysis.basic_facts Require Export service.
 
 From rt.util Require Import nat.
diff --git a/restructuring/analysis/basic_facts/deadlines.v b/restructuring/analysis/basic_facts/deadlines.v
index 1196bd3e3e328e82c10f8be6308c3b237aeed632..7fe7696ffa8c84970516fa9c471c72deb7daa785 100644
--- a/restructuring/analysis/basic_facts/deadlines.v
+++ b/restructuring/analysis/basic_facts/deadlines.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.analysis.basic_facts Require Export service completion.
 
 (** In this file, we observe basic properties of the behavioral job
diff --git a/restructuring/analysis/basic_facts/service.v b/restructuring/analysis/basic_facts/service.v
index 9b3c2cf3185edc3733b91a87be9d471bbecafc4b..44539d945ebb06a24debeff8388f9bc0e46bd884 100644
--- a/restructuring/analysis/basic_facts/service.v
+++ b/restructuring/analysis/basic_facts/service.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model.processor Require Export platform_properties.
 From rt.util Require Import tactics step_function sum.
 
diff --git a/restructuring/analysis/basic_facts/service_of_jobs.v b/restructuring/analysis/basic_facts/service_of_jobs.v
index 3924225e08901268e6352d0126439aa992cba8e2..4e84ffafe29b327ba3dd3f90f3aae7cb8fbfd9f4 100644
--- a/restructuring/analysis/basic_facts/service_of_jobs.v
+++ b/restructuring/analysis/basic_facts/service_of_jobs.v
@@ -1,5 +1,5 @@
 From rt.util Require Import tactics sum.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Import service.
 From rt.restructuring.model Require Export service_of_jobs.
 From rt.restructuring.model Require Import task schedule.priority_based.priorities processor.ideal.
 From rt.restructuring.analysis Require Import workload.
@@ -255,10 +255,10 @@ Section IdealModelLemmas.
         rewrite /workload_of_jobs in EQ.
         rewrite (big_rem j) ?Pj //= in EQ.
         move: EQ => /eqP; rewrite addn_eq0; move => /andP [CZ _].
-        unfold completed_by, schedule.completed_by.
+        unfold completed_by, service.completed_by.
           by move: CZ => /eqP CZ; rewrite CZ. 
       }
-      { unfold workload_of_jobs, service_of_jobs in EQ; unfold completed_by, schedule.completed_by.
+      { unfold workload_of_jobs, service_of_jobs in EQ; unfold completed_by, service.completed_by.
         rewrite /service -(service_during_cat _ _ _ t1); last by apply/andP; split. 
         rewrite cumulative_service_before_job_arrival_zero // add0n.
         rewrite <- sum_majorant_eqn with (F1 := fun j => service_during sched j t1 t_compl)
diff --git a/restructuring/analysis/schedulability.v b/restructuring/analysis/schedulability.v
index 7226af67427d5305edee46f132893562b7a838be..0e332a9e319ec3e48a7e28df59547da3d81a65e7 100644
--- a/restructuring/analysis/schedulability.v
+++ b/restructuring/analysis/schedulability.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Export task.
 From rt.restructuring.analysis.basic_facts Require Export completion.
 From rt.util Require Export seqset.
diff --git a/restructuring/analysis/task_schedule.v b/restructuring/analysis/task_schedule.v
index 8bc83c0f00f96e58d8d09171c0874a0248fdcf2a..dd846c6e3a49d1ecef0c5dac7aec462fd1296c7b 100644
--- a/restructuring/analysis/task_schedule.v
+++ b/restructuring/analysis/task_schedule.v
@@ -1,5 +1,5 @@
 From rt.restructuring.model Require Import task.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.analysis.basic_facts Require Import ideal_schedule.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/transform/prefix.v b/restructuring/analysis/transform/prefix.v
index 2187ebe2a50c4baf1e5c029475f7d073d52a691e..d006258566f0edb297bac244366f4abf7693b96a 100644
--- a/restructuring/analysis/transform/prefix.v
+++ b/restructuring/analysis/transform/prefix.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.analysis Require Import basic_facts.all.
 
 (** This file provides an operation that transforms a finite prefix of
diff --git a/restructuring/analysis/transform/swap.v b/restructuring/analysis/transform/swap.v
index 6f32fc7d364101417713597bcb23ac69171c86d3..f44a4055705f0572d16069001b00c5fdcfc902da 100644
--- a/restructuring/analysis/transform/swap.v
+++ b/restructuring/analysis/transform/swap.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule job.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.analysis.basic_facts Require Import all.
 
 (** This file defines simple allocation substitutions and a swapping operation
diff --git a/restructuring/analysis/workload.v b/restructuring/analysis/workload.v
index 453d1e2819eb56313b6be174118afd80fca6a937..aab4291b21300dc3918cce285ba719766e90cf69 100644
--- a/restructuring/analysis/workload.v
+++ b/restructuring/analysis/workload.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Export workload schedule.priority_based.priorities.
 From rt.restructuring.analysis Require Import basic_facts.arrivals.
 
diff --git a/restructuring/behavior/all.v b/restructuring/behavior/all.v
new file mode 100644
index 0000000000000000000000000000000000000000..f12642cbe3dadf6371e8d36be6bcae1112fd7d7d
--- /dev/null
+++ b/restructuring/behavior/all.v
@@ -0,0 +1,6 @@
+Require Export rt.restructuring.behavior.time.
+Require Export rt.restructuring.behavior.job.
+Require Export rt.restructuring.behavior.arrival_sequence.
+Require Export rt.restructuring.behavior.schedule.
+Require Export rt.restructuring.behavior.service.
+Require Export rt.restructuring.behavior.ready.
diff --git a/restructuring/behavior/ready.v b/restructuring/behavior/ready.v
new file mode 100644
index 0000000000000000000000000000000000000000..2a5c9773d35cb59fd81018c7692ab4cf8d413706
--- /dev/null
+++ b/restructuring/behavior/ready.v
@@ -0,0 +1,75 @@
+From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
+From rt.restructuring.behavior Require Export service.
+
+
+(* We define a general notion of readiness of a job: a job can be
+   scheduled only when it is ready. This notion of readiness is a general
+   concept that is used to model jitter, self-suspensions, etc.  Crucially, we
+   require that any sensible notion of readiness is a refinement of the notion
+   of a pending job, i.e., any ready job must also be pending. *)
+Class JobReady (Job : JobType) (PState : Type)
+      `{ProcessorState Job PState} `{JobCost Job} `{JobArrival Job} :=
+  {
+    job_ready : schedule PState -> Job -> instant -> bool;
+    any_ready_job_is_pending : forall sched j t, job_ready sched j t -> pending sched j t;
+  }.
+
+(* Based on the general notion of readiness, we define what it means to be
+   backlogged, i.e., ready to run but not executing. *)
+Section Backlogged.
+  (* Conside any kinds of jobs and any kind of processor state. *)
+  Context {Job : JobType} {PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  (* Allow for any notion of readiness. *)
+  Context `{JobReady Job PState}.
+
+  (* Job j is backlogged at time t iff it is ready and not scheduled. *)
+  Definition backlogged (sched : schedule PState) (j : Job) (t : instant) :=
+    job_ready sched j t && ~~ scheduled_at sched j t.
+
+End Backlogged.
+
+
+(* With the readiness concept in place, we define the notion of valid schedules. *)
+Section ValidSchedule.
+  (* Consider any kinds of jobs and any kind of processor state. *)
+  Context {Job : JobType} {PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  (* Consider any schedule. *)
+  Variable sched : schedule PState.
+
+  Context `{JobArrival Job}.
+
+  (* We define whether jobs come from some arrival sequence... *)
+  Definition jobs_come_from_arrival_sequence (arr_seq : arrival_sequence Job) :=
+    forall j t, scheduled_at sched j t -> arrives_in arr_seq j.
+
+  (* ..., whether a job can only be scheduled if it has arrived ... *)
+  Definition jobs_must_arrive_to_execute :=
+    forall j t, scheduled_at sched j t -> has_arrived j t.
+
+  Context `{JobCost Job}.
+  Context `{JobReady Job PState}.
+
+  (* ..., whether a job can only be scheduled if it is ready ... *)
+  Definition jobs_must_be_ready_to_execute :=
+    forall j t, scheduled_at sched j t -> job_ready sched j t.
+
+  (* ... and whether a job cannot be scheduled after it completes. *)
+  Definition completed_jobs_dont_execute :=
+    forall j t, scheduled_at sched j t -> service sched j t < job_cost j.
+
+  (* We say that the schedule is valid iff
+     - jobs come from some arrival sequence
+     - a job is scheduled if it is ready *)
+  Definition valid_schedule (arr_seq : arrival_sequence Job) :=
+    jobs_come_from_arrival_sequence arr_seq /\
+    jobs_must_be_ready_to_execute.
+
+  (* Note that we do not explicitly require that a valid schedule satisfies
+     jobs_must_arrive_to_execute or completed_jobs_dont_execute because these
+     properties are implied by jobs_must_be_ready_to_execute. *)
+
+End ValidSchedule.
diff --git a/restructuring/behavior/schedule.v b/restructuring/behavior/schedule.v
index 71d4153f5b8fef064a048ab9125a7ad4669983fc..d52e29116bbe664259241b92a5b2c6e56c85d29a 100644
--- a/restructuring/behavior/schedule.v
+++ b/restructuring/behavior/schedule.v
@@ -22,132 +22,3 @@ Class ProcessorState (Job : JobType) (State : Type) :=
 (* A schedule maps an instant to a processor state *)
 Definition schedule (PState : Type) := instant -> PState.
 
-Section Schedule.
-  Context {Job : JobType} {PState : Type}.
-  Context `{ProcessorState Job PState}.
-
-  Variable sched : schedule PState.
-
-  (* First, we define whether a job j is scheduled at time t, ... *)
-  Definition scheduled_at (j : Job) (t : instant) := scheduled_in j (sched t).
-
-  (* ... and the instantaneous service received by
-           job j at time t. *)
-  Definition service_at (j : Job) (t : instant) := service_in j (sched t).
-
-  (* Based on the notion of instantaneous service, we define the
-           cumulative service received by job j during any interval [t1, t2). *)
-  Definition service_during (j : Job) (t1 t2 : instant) :=
-    \sum_(t1 <= t < t2) service_at j t.
-
-  (* Using the previous definition, we define the cumulative service
-           received by job j up to time t, i.e., during interval [0, t). *)
-  Definition service (j : Job) (t : instant) := service_during j 0 t.
-
-  Context `{JobCost Job}.
-  Context `{JobDeadline Job}.
-  Context `{JobArrival Job}.
-
-  (* Next, we say that job j has completed by time t if it received enough
-           service in the interval [0, t). *)
-  Definition completed_by (j : Job) (t : instant) := service j t >= job_cost j.
-
-  (* We say that job j completes at time t if it has completed by time t but
-     not by time t - 1 *)
-  Definition completes_at (j : Job) (t : instant) := ~~ completed_by j t.-1 && completed_by j t.
-
-  (* We say that R is a response time bound of a job j if j has completed
-     by R units after its arrival *)
-  Definition job_response_time_bound (j : Job) (R : duration) :=
-    completed_by j (job_arrival j + R).
-
-  (* We say that a job meets its deadline if it completes by its absolute deadline *)
-  Definition job_meets_deadline (j : Job) :=
-    completed_by j (job_deadline j).
-
-  (* Job j is pending at time t iff it has arrived but has not yet completed. *)
-  Definition pending (j : Job) (t : instant) := has_arrived j t && ~~ completed_by j t.
-
-  (* Job j is pending earlier and at time t iff it has arrived before time t
-           and has not been completed yet. *)
-  Definition pending_earlier_and_at (j : Job) (t : instant) :=
-    arrived_before j t && ~~ completed_by j t.
-
-  (* Let's define the remaining cost of job j as the amount of service
-     that has to be received for its completion. *)
-  Definition remaining_cost j t :=
-    job_cost j - service j t.
-
-End Schedule.
-
-(* We next define a general notion of readiness of a job: a job can be
-   scheduled only when it is ready. This notion of readiness is a general
-   concept that is used to model jitter, self-suspensions, etc.  Crucially, we
-   require that any sensible notion of readiness is a refinement of the notion
-   of a pending job, i.e., any ready job must also be pending. *)
-Class JobReady (Job : JobType) (PState : Type)
-      `{ProcessorState Job PState} `{JobCost Job} `{JobArrival Job} :=
-  {
-    job_ready : schedule PState -> Job -> instant -> bool;
-    any_ready_job_is_pending : forall sched j t, job_ready sched j t -> pending sched j t;
-  }.
-
-(* Based on the general notion of readiness, we define what it means to be
-   backlogged, i.e., ready to run but not executing. *)
-Section Backlogged.
-  (* Conside any kinds of jobs and any kind of processor state. *)
-  Context {Job : JobType} {PState : Type}.
-  Context `{ProcessorState Job PState}.
-
-  (* Allow for any notion of readiness. *)
-  Context `{JobReady Job PState}.
-
-  (* Job j is backlogged at time t iff it is ready and not scheduled. *)
-  Definition backlogged (sched : schedule PState) (j : Job) (t : instant) :=
-    job_ready sched j t && ~~ scheduled_at sched j t.
-
-End Backlogged.
-
-
-(* In this section, we define valid schedules. *)
-Section ValidSchedule.
-  (* Consider any kinds of jobs and any kind of processor state. *)
-  Context {Job : JobType} {PState : Type}.
-  Context `{ProcessorState Job PState}.
-
-  (* Consider any schedule. *)
-  Variable sched : schedule PState.
-
-  Context `{JobArrival Job}.
-
-  (* We define whether jobs come from some arrival sequence... *)
-  Definition jobs_come_from_arrival_sequence (arr_seq : arrival_sequence Job) :=
-    forall j t, scheduled_at sched j t -> arrives_in arr_seq j.
-
-  (* ..., whether a job can only be scheduled if it has arrived ... *)
-  Definition jobs_must_arrive_to_execute :=
-    forall j t, scheduled_at sched j t -> has_arrived j t.
-
-  Context `{JobCost Job}.
-  Context `{JobReady Job PState}.
-
-  (* ..., whether a job can only be scheduled if it is ready ... *)
-  Definition jobs_must_be_ready_to_execute :=
-    forall j t, scheduled_at sched j t -> job_ready sched j t.
-
-  (* ... and whether a job cannot be scheduled after it completes. *)
-  Definition completed_jobs_dont_execute :=
-    forall j t, scheduled_at sched j t -> service sched j t < job_cost j.
-
-  (* We say that the schedule is valid iff
-     - jobs come from some arrival sequence
-     - a job is scheduled if it is ready *)
-  Definition valid_schedule (arr_seq : arrival_sequence Job) :=
-    jobs_come_from_arrival_sequence arr_seq /\
-    jobs_must_be_ready_to_execute.
-
-  (* Note that we do not explicitly require that a valid schedule satisfies
-     jobs_must_arrive_to_execute or completed_jobs_dont_execute because these
-     properties are implied by jobs_must_be_ready_to_execute. *)
-
-End ValidSchedule.
diff --git a/restructuring/behavior/service.v b/restructuring/behavior/service.v
new file mode 100644
index 0000000000000000000000000000000000000000..e3378055565d97cad06404432be204fc974e340c
--- /dev/null
+++ b/restructuring/behavior/service.v
@@ -0,0 +1,60 @@
+From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
+From rt.restructuring.behavior Require Export schedule.
+
+Section Service.
+  Context {Job : JobType} {PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  Variable sched : schedule PState.
+
+  (* First, we define whether a job j is scheduled at time t, ... *)
+  Definition scheduled_at (j : Job) (t : instant) := scheduled_in j (sched t).
+
+  (* ... and the instantaneous service received by
+           job j at time t. *)
+  Definition service_at (j : Job) (t : instant) := service_in j (sched t).
+
+  (* Based on the notion of instantaneous service, we define the
+           cumulative service received by job j during any interval [t1, t2). *)
+  Definition service_during (j : Job) (t1 t2 : instant) :=
+    \sum_(t1 <= t < t2) service_at j t.
+
+  (* Using the previous definition, we define the cumulative service
+           received by job j up to time t, i.e., during interval [0, t). *)
+  Definition service (j : Job) (t : instant) := service_during j 0 t.
+
+  Context `{JobCost Job}.
+  Context `{JobDeadline Job}.
+  Context `{JobArrival Job}.
+
+  (* Next, we say that job j has completed by time t if it received enough
+           service in the interval [0, t). *)
+  Definition completed_by (j : Job) (t : instant) := service j t >= job_cost j.
+
+  (* We say that job j completes at time t if it has completed by time t but
+     not by time t - 1 *)
+  Definition completes_at (j : Job) (t : instant) := ~~ completed_by j t.-1 && completed_by j t.
+
+  (* We say that R is a response time bound of a job j if j has completed
+     by R units after its arrival *)
+  Definition job_response_time_bound (j : Job) (R : duration) :=
+    completed_by j (job_arrival j + R).
+
+  (* We say that a job meets its deadline if it completes by its absolute deadline *)
+  Definition job_meets_deadline (j : Job) :=
+    completed_by j (job_deadline j).
+
+  (* Job j is pending at time t iff it has arrived but has not yet completed. *)
+  Definition pending (j : Job) (t : instant) := has_arrived j t && ~~ completed_by j t.
+
+  (* Job j is pending earlier and at time t iff it has arrived before time t
+           and has not been completed yet. *)
+  Definition pending_earlier_and_at (j : Job) (t : instant) :=
+    arrived_before j t && ~~ completed_by j t.
+
+  (* Let's define the remaining cost of job j as the amount of service
+     that has to be received for its completion. *)
+  Definition remaining_cost j t :=
+    job_cost j - service j t.
+
+End Service.
diff --git a/restructuring/model/aggregate/service_of_jobs.v b/restructuring/model/aggregate/service_of_jobs.v
index 7aab4cdad6a74bfc3fad3e66eaee3819c569e1a9..b8ade10471fe442d3f7b205abc42fac2f59cb791 100644
--- a/restructuring/model/aggregate/service_of_jobs.v
+++ b/restructuring/model/aggregate/service_of_jobs.v
@@ -1,5 +1,5 @@
 From rt.util Require Import tactics sum.
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Import task schedule.priority_based.priorities processor.ideal.
 From rt.restructuring.analysis Require Import workload.
 From rt.restructuring.analysis.basic_facts Require Import arrivals completion ideal_schedule.
diff --git a/restructuring/model/aggregate/workload.v b/restructuring/model/aggregate/workload.v
index 891124dd2fdc1bf17807010b8bbaeca8103e17c5..0160115f3e066a81c86e48e43bf7ba7bb4a48d0c 100644
--- a/restructuring/model/aggregate/workload.v
+++ b/restructuring/model/aggregate/workload.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Import task schedule.priority_based.priorities.
 From rt.restructuring.analysis Require Import basic_facts.arrivals.
 
diff --git a/restructuring/model/arrival/arrival_curves.v b/restructuring/model/arrival/arrival_curves.v
index e33d68c96fc4d8ef3b7a4cfa7cf1e0942a208a0b..4a7c2bf6273925ed455f4ebc6fe4475e15cce448 100644
--- a/restructuring/model/arrival/arrival_curves.v
+++ b/restructuring/model/arrival/arrival_curves.v
@@ -1,5 +1,5 @@
 From rt.util Require Import all.
-From rt.restructuring.behavior Require Export arrival_sequence.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Import task_arrivals.
 
 (* In this section, we define the notion of arrival curves, which
diff --git a/restructuring/model/arrival/sporadic.v b/restructuring/model/arrival/sporadic.v
index a0b1c60c316236daacd845afc2e347105ce7ab37..fb19b8d1eb6618d7de27ac393acd96c05c84a089 100644
--- a/restructuring/model/arrival/sporadic.v
+++ b/restructuring/model/arrival/sporadic.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export arrival_sequence.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Export task.
 
 Section TaskMinInterArrivalTime.
diff --git a/restructuring/model/job.v b/restructuring/model/job.v
index 40ddc1a91dea6a5674dee8b51ef162f89df387ea..9701ef4854009289da46ca164a3d8519516a077a 100644
--- a/restructuring/model/job.v
+++ b/restructuring/model/job.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export time job.
+From rt.restructuring.behavior Require Export all.
 From mathcomp Require Export eqtype ssrnat.
 
 (* In this section, we introduce properties of a job. *)
diff --git a/restructuring/model/preemption/preemption_model.v b/restructuring/model/preemption/preemption_model.v
index d60e9903a50d50d4f19b5fda722ddf884db2abd7..0669e2cfa148baac902b87ac934f6fe319a57749 100644
--- a/restructuring/model/preemption/preemption_model.v
+++ b/restructuring/model/preemption/preemption_model.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Import job schedule.
+From rt.restructuring.behavior Require Import all.
 From rt.restructuring.model Require Import job task.
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/model/processor/ideal.v b/restructuring/model/processor/ideal.v
index a08ca228ec8a46794cf8117e152acf5b8a36b87d..ca65de81f8f96ca5258e1aebe13e6f8165da1e25 100644
--- a/restructuring/model/processor/ideal.v
+++ b/restructuring/model/processor/ideal.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
 
 (** First let us define the notion of an ideal schedule state, as done in Prosa
     so far: either a job is scheduled or the system is idle. *)
diff --git a/restructuring/model/processor/multiprocessor.v b/restructuring/model/processor/multiprocessor.v
index f9a4dc60d85e216f5e6dbc5c12d4a6f0056195b1..f84a7d6dbfeea2dd21cca930400ba7f83e31f434 100644
--- a/restructuring/model/processor/multiprocessor.v
+++ b/restructuring/model/processor/multiprocessor.v
@@ -1,5 +1,5 @@
 From mathcomp Require Export fintype.
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
 
 Section Schedule.
 
diff --git a/restructuring/model/processor/platform_properties.v b/restructuring/model/processor/platform_properties.v
index dedc5544e22467012ed19ab9edfc12a30406f84b..1ad0b7cb0fa01046f8ba42ca894270ae37120b5d 100644
--- a/restructuring/model/processor/platform_properties.v
+++ b/restructuring/model/processor/platform_properties.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
 
 (* To reason about classes of schedule types / processor models, we define the
    following properties that a processor model might possess. *)
diff --git a/restructuring/model/processor/spin.v b/restructuring/model/processor/spin.v
index 12108fc33cdd8edcaf0792fcbc7fa1fb1afd3655..44826d232cc7b76c011be60b4a29ea2b9b287785 100644
--- a/restructuring/model/processor/spin.v
+++ b/restructuring/model/processor/spin.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
 
 (** Next we define a processor state that includes the possibility of spinning,
     where spinning jobs do not progress (= don't get service). *)
diff --git a/restructuring/model/processor/varspeed.v b/restructuring/model/processor/varspeed.v
index b31855d7fe2c8998479508e84a9cde9887c20c74..2708b14902cccde2626a89f4ac96dcc001be31b0 100644
--- a/restructuring/model/processor/varspeed.v
+++ b/restructuring/model/processor/varspeed.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
 
 (** Next, let us define a schedule with variable execution speed. *)
 Section State.
diff --git a/restructuring/model/readiness/basic.v b/restructuring/model/readiness/basic.v
index ccda30e461d77f017c2eaacf34179526002c692c..6b16bfab608aa2a3890d74d855430156d441d287 100644
--- a/restructuring/model/readiness/basic.v
+++ b/restructuring/model/readiness/basic.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.analysis.basic_facts Require Import completion.
 
 (* We define the readiness indicator function for the classic Liu & Layland
diff --git a/restructuring/model/readiness/jitter.v b/restructuring/model/readiness/jitter.v
index 49e5e2e6a5b455449d0430a1e8c2272ee963f430..a61b7a6b1637707bcf33ea4ccf7cb6b6216e28cb 100644
--- a/restructuring/model/readiness/jitter.v
+++ b/restructuring/model/readiness/jitter.v
@@ -1,5 +1,5 @@
 From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
 
 From rt.util Require Import nat.
 
diff --git a/restructuring/model/schedule/edf.v b/restructuring/model/schedule/edf.v
index 5ba654c221137889bd834d8eff7ec0e13a1ae86a..90c09b19f19baabd806e759bc71bf8ff64937ea6 100644
--- a/restructuring/model/schedule/edf.v
+++ b/restructuring/model/schedule/edf.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
 
 (** In this file, we define what it means to be an "EDF schedule". *)
 Section DefinitionOfEDF.
diff --git a/restructuring/model/schedule/priority_based/preemptive.v b/restructuring/model/schedule/priority_based/preemptive.v
index c8d265402d14ef11b13f4b2d4c0d93debe71c65a..2bfcdf195fbb284a49f7cf96367f9b048519214b 100644
--- a/restructuring/model/schedule/priority_based/preemptive.v
+++ b/restructuring/model/schedule/priority_based/preemptive.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule arrival_sequence.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Export priorities.
 
 (* We now define what it means for a schedule to respect a priority *)
diff --git a/restructuring/model/schedule/sequential.v b/restructuring/model/schedule/sequential.v
index 664414f6dec1aa7dae10368683772ccfc80dbfde..08c91c41b557d614b8e4132ab3435841329b6698 100644
--- a/restructuring/model/schedule/sequential.v
+++ b/restructuring/model/schedule/sequential.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model Require Export task.
 
 Section PropertyOfSequentiality.
diff --git a/restructuring/model/schedule/work_conserving.v b/restructuring/model/schedule/work_conserving.v
index a37e357a728b14fd7fa169d3ce58e28e5e9b71ec..e5447011b7b26907ffe999662e7b44b428e8ccf8 100644
--- a/restructuring/model/schedule/work_conserving.v
+++ b/restructuring/model/schedule/work_conserving.v
@@ -1,4 +1,4 @@
-From rt.restructuring.behavior Require Export schedule arrival_sequence.
+From rt.restructuring.behavior Require Export all.
 
 (* In this file, we introduce a restrictive definition of work conserving
    uniprocessor schedules. The definition is restrictive because it does not
diff --git a/restructuring/model/task.v b/restructuring/model/task.v
index b325e42d6e59c2b150a42ec6851f56be14909953..f25bdb465f277ebdee5d20dc8e427d3cc24c4ad2 100644
--- a/restructuring/model/task.v
+++ b/restructuring/model/task.v
@@ -1,6 +1,5 @@
 From mathcomp Require Export ssrbool.
-From rt.restructuring.behavior Require Export job.
-From rt.restructuring.behavior Require Export arrival_sequence.
+From rt.restructuring.behavior Require Export all.
   
 (* Throughout the library we assume that tasks have decidable equality *)
 Definition TaskType := eqType.