diff --git a/analysis/definitions/completion_sequence.v b/analysis/definitions/completion_sequence.v
new file mode 100644
index 0000000000000000000000000000000000000000..d53960d6527a35c2cb51bcf5f568b80f0c0e1708
--- /dev/null
+++ b/analysis/definitions/completion_sequence.v
@@ -0,0 +1,28 @@
+From mathcomp Require Export ssreflect seq ssrnat ssrbool eqtype.
+Require Import prosa.behavior.service.
+
+(** This module contains basic definitions and properties of job
+    completion sequences. *)
+
+(** * Notion of a Completion Sequence *)
+
+(** We begin by defining a job completion sequence. *)
+Section CompletionSequence.
+
+  (** Consider any kind of jobs with a cost
+     and any kind of processor state. *)
+  Context {Job : JobType} `{JobCost Job} {PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  (** Consider any job arrival sequence. *)
+  Variable arr_seq: arrival_sequence Job.
+
+  (** Consider any schedule. *)
+  Variable sched : schedule PState.
+
+  (** For each instant [t], the completion sequence returns all
+     arrived jobs that have completed at [t]. *)
+  Definition completion_sequence : arrival_sequence Job :=
+    fun t => [seq j <- arrivals_up_to arr_seq t | completes_at sched j t].
+
+End CompletionSequence.