diff --git a/specification.m b/specification.m
new file mode 100644
index 0000000000000000000000000000000000000000..cf119176effe688a03fd3c3d4ca6fb750950c08f
--- /dev/null
+++ b/specification.m
@@ -0,0 +1,50 @@
+%% Tutorial example on symbolic control
+%% Author: Antoine GIRARD, Université Paris-Saclay, CNRS, CentraleSupélec, Laboratoire des signaux et systèmes, 91190, Gif-sur-Yvette, France.
+%% Date: 2024
+
+%% Definition of the specification
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Specification
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Regions of interest and labeling function
+
+% Assumption on the regions of interest: 
+% 1) State partition cells are either completely inside or completely outside any region of interest
+% 2) Two regions of of interest do not intersect
+
+R1=[4 5; 8.5 9.5;-pi pi];
+R2=[8.5 9.5; 2 3;-pi pi];
+R3=[2 3; 0.5 1.5;-pi pi];
+R4=[3 7; 3 7;-pi pi];
+
+% Labeling function: 1 - not in any region; 2 - R1; 3 - R2; 4 - R3; 5 - R4
+
+Lab_x=@(x) 1+...
+          1*(all(x>=R1(:,1)) & all(x<=R1(:,2)))+...
+          2*(all(x>=R2(:,1)) & all(x<=R2(:,2)))+...
+          3*(all(x>=R3(:,1)) & all(x<=R3(:,2)))+...
+          4*(all(x>=R4(:,1)) & all(x<=R4(:,2)));
+
+% Specification automaton:
+
+% Transition relation
+% rows (automaton states) / column (labels) 
+% value (next automaton state)
+
+A_s=[1 2 3 1 5;...
+     2 2 5 4 5;...
+     3 5 3 4 5;...
+     4 4 4 4 4;...
+     5 5 5 5 5];
+
+ 
+n_s=length(A_s);
+
+% Initial state
+I_s=1;
+
+% Final states
+F_s=[4];
+