Logic and Automated Reasoning (LAR) 2023-2024
ASSIGNMENT
PARTS:
The LAR assignment is divided in three parts, all to be attempted:
· PART I [80 points] on Propositional Logic, FOL, Formal Models,
Model Checking, and TLA+.
· PART II [10 points] and PART III[10 points] on Causal Inference
and Machine Learning.
RATIONALE:
PART I aims at:
· Produce a Formal Model (as a State Machine) of an assigned
engineering problem.
· Implement all the requirements provided as Specs, Steps and
Properties using the software TLA+ and its Toolbox
(Toolbox download available at
· Programme the TLA+ Toolbox Model Checker to find the solution
of the given problem.
PART II aims at:
· Produce a critical review on a recent research article about causal
inference and machine learning.
PART III aims at:
· Verify the hands-on comprehension of concepts introduced during
the module.
LIST OF DELIVERABLES:
The list of deliverables to be uploaded on Turnitin is:
One single, zipped folder containing all the files below (1. 2. And 3.).
You shall submit all the Part I,II and III files in one single file through
Canvas.
1. Part I: Code.
A single, zipped folder containing a single .tla file, and all files,
codes, scripts and functions to run the assigned exercise.
Make sure the submitted script can be opened and works, and
that you include in the submission all necessary functions
and files.
Zip all your files and put them in the folder to be submitted in
canvas.
REMARK: If the Model or Model Checker files cannot be correctly
opened, saved (with green light “parsed” appearing) or run, the
assignment will be marked as REVISE and REPRESENT or FAIL.
REMARK: submit all your code in a single .zip file named
LAR24SXXXXXX.zip where XXXXXX is your student number (e.g.:
LAR24S000000.zip)
REMARK: make sure the zipped folder contains one single .tla
file to avoid ambiguity on the file to be marked.
2. PART II: Typed Report.
A Word document containing the critical review with all parts as
described below. The document length should be between 1 and 2
A4 pages and should use Arial 11pt font. Any content beyond this
space will NOT be evaluated.
REMARK: This PART of the assignment assesses the personal
ability to understand, critique and relate to previous concepts. The
use of AI tools infringes its rules and will be considered a case of
academic misconduct.
3. PART II: Typed Answer.
A word file containing the requested list.
PART I
Engineering problem statement:
A spacecraft is in orbit around the Earth at an altitude (distance from the
ground) of 300 km.
It is equipped with solar panels, getting electric energy from the Sun to
be used directly to run the thrusters or stored in a battery.
The spacecraft has electric thrusters that can use either the energy from
the solar panels or the one stored in the battery.
Turning on the thrusters raises the altitude of the spacecraft.
Each orbit (anti-clockwise) is represented as a full cycle of light
conditions (see Figure 1) encountered by the spacecraft.
Light condition will thus loop over the following values (in order):
PENUMBRA (initial state) ⟹ ECLIPSE ⟹ PENUMBRA ⟹ SUNLIGHT
This will be referred hereafter as a light condition cycle or loop.
At the end of each cycle, the light conditions loop will start over (i.e.:
from the SUNLIGHT condition to the one PENUMBRA).
At the end of each full cycle of light condition (i.e.: from the SUNLIGHT
condition to the one PENUMBRA) the spacecraft has completed an orbit,
and the orbit count will raise of 1.
PENUMBRA
ECLIPSE
SUNLIGHT EARTH
PENUMBRA
SUN
Fig. 1
AIM:
- Following all the Specs, Steps and Properties listed in the Table 1
below, produce a guided Formal Model of the spacecraft’s orbit
raising problem as a State Machine.
- Design a function to check that all variables span the right values as
per Specs below.
- Use the Model Checker to determine what is the maximum
reachable altitude in 4 orbits for the model developed.
Table 1: Specs, Steps and Properties.
CODE Requirement POINTS
FORM.0 It shall be possible to correctly open, save
(with green “parsed” light appearing) and
run both Model and Model Checker files.
FAILING to
provide this
requirement
will result in
REVISE and
REPRESENT
Or
FAIL
Both Model and Model Checker files, when
parsed and run shall not provide errors.
FORM.1 All the relevant files have been submitted in
a single .ZIP file named
LAR24SXXXXXX.zip where XXXXXX is
your student number (e.g.:
LAR24S000000.zip).
The zipped folder contains a single .tla file.
The .tla file named LAR24SXXXXXX.tla
with XXXXXX is your student number (e.g.:
LAR24S000000.tla).
The code shall be divided in relevant
sections (using comments ).
The code shall be commented with
relevant, correct, and clear comments.
The general layout of the code shall be
readable, tidy, and easy to follow, with all
operators coherently indented, tabbed and
spaced.
Both the Model and Model Checker files,
when saved, parsed and run shall not
provide warnings.
FORM.2 The model shall use the sole variables:
· LIGHTCONDITION
· BATTERYCHARGE
· ALTITUDE
· ORBITNUMBER
· THRUSTERS
· PREVIOUSLIGHTCONDITION
All variables shall be in capital letters.
LIGHTCONDITION shall span over the sole
following values:
“SUNLIGHT”, “PENUMBRA”, “ECLIPSE”.
PREVIOUSLIGHTCONDITION shall span
over the sole following values:
“SUNLIGHT”, “PENUMBRA”, “ECLIPSE”.
BATTERYCHARGE shall span over the
sole following values:
integer values from 0 to 4 (extremal
included).
Where 4 is the fully charged state, 0 is the
empty state.
��� ∈ [0, 4] ⊂ ℕ+
ALTITUDE shall span over the sole
following values:
the “hundred” values from 300 on, namely
300, 400, 500, 600, 700, …
��� = 300 + 100 ���, with ��� ∈ ℕ+
ORBITNUMBER shall span over the sole
following values:
integer values from 1 on, namely 1, 2, 3, 4,
5, 6, …
��� ∈ ℕ+ \{0}
THRUSTERS shall span over the sole
following values:
“ON”, “OFF”.
All values of the variables shall be in capital
letters.
FORM.3 The ORBITNUMBER shall start from 1. 10
The spacecraft shall start at an ALTITUDE of
The spacecraft LIGHTCONDITION shall
start from the “PENUMBRA” state (see
Fig.1).
The spacecraft
PREVIOUSLIGHTCONDITION shall start
from the “SUNLIGHT” state (see Fig.1).
The spacecraft shall start with THRUSTERS
“OFF”.
The spacecraft shall start with BATTERY
fully charged.
The Next function shall be a disjunction of
the Steps listed below.
The sole Steps allowed to change the state
of the system are:
· RAISE
· CHARGE
· RAISEANDCHARGE
· SYSTEMSOFF.
All Steps names shall be in capital letters.
Each Step shall fully define the arrival status
of all variables.
Raising the orbit of the spacecraft shall be
performed solely by selecting one among the
RAISE and RAISEANDCHARGE Steps.
Charging the battery of the spacecraft will be
performed solely by one among the
CHARGE and RAISEANDCHARGE Steps.
The SYSTEMSOFF Step shall not raise the
orbit altitude nor charge the battery status.
MC.1 A TYPEOK function shall be implemented
to check that variable values for all states
are always contained in the right sets,
defined in requirement FORM.2.
The function name TYPEOK shall be in
capital letters.
The TYPEOK function shall be coded in the
Model code (i.e.: the .tla file).
The function TYPEOK shall be only called
from the Model Checker, adding the sole
word TYPEOK to the Model Checker as an
Invariant.
Running the Model Checker with Invariant
TYPEOK flagged, the software shall not
produce any violation of the Invariant
TYPEOK.
The number of “Distinct States” (see Fig.2)
found from the Model Checker shall not
change when running the model checker
multiple times.
After running the Model Checker, the
Actions column of the Model Checking
results Tab (see Fig.3) shall report all the 4
steps reported in the requirement FORM.1
After running the Model Checker, the
occurrence of the Distinct States of the
different Actions in the Model Checking
results Tab (see Fig.4) shall be compatible
with the systems specification requirements
(STEPS.1).
SPECS.1 The light condition status of the spacecraft
shall change at every state change (i.e.:
independently from the Step selected).
The light condition of the spacecraft loops
following (in order) the light condition cycle:
PENUMBRA ⟹ECLIPSE ⟹ PENUMBRA
⟹SUNLIGHT
And then starts over (as per Figure 1).
SPECS.2 The value of the light condition the
spacecraft in the previous status (the status
immediately before the current one) shall be
stored as the
PREVIOUSLIGHTCONDITION of the
current status.
The orbit number shall increase by 1 at the
beginning of each new light condition cycle.
(Namely, the orbit number shall be added a
+1 every time the previous light condition
status transitions to SUNLIGHT.)
Raising the orbit shall transition of the
thrusters’ state to ON (independently if you
are also charging the battery or not).
All Steps in which the spacecraft is not
raising its orbit shall transition the thrusters
state to OFF.
STEPS.1 Raising the orbit shall higher the altitude of
the spacecraft of:
· +200 if the spacecraft is in sunlight
and not charging the battery.
· +100 elsewhere.
Raising the orbit in ECLIPSE or
PENUMBRA shall decrease your battery
charge of 2
Namely the battery charge shall be
summed a -2
Charging the battery will higher the level of
the battery of:
· +2 if the spacecraft is in sunlight and
not raising its orbit.
· +1 elsewhere.
Not raising the orbit shall leave the altitude
status unchanged.
Not charging the battery shall leave the
battery status unchanged.
PROP.1 Battery shall never charge when the
spacecraft is in eclipse.
The spacecraft in penumbra shall either
charge its battery or raise its altitude but
cannot perform both.
Charging a fully charged battery shall leave
the battery charge unchanged.
RES.1 Calling ��� the limit magnitude, i.e.: the
highest altitude reachable in 4 orbits, the
spacecraft shall be able to reach all the
altitudes ≤ ���.
Calling ��� the highest altitude reachable in 4
orbits, the spacecraft shall not be able to
reach any altitude > ���.
a LIMITALTITUDE function shall be
implemented to demonstrate that the
spacecraft can reach a certain limit altitude
��� in 4 orbits.
The function name LIMITALTITUDE shall
be in capital letters.
The LIMITALTITUDE function shall be
coded in the Model code (i.e.: the .tla file).
The function LIMITALTITUDE shall be only
added to the Model Checker Invariants by
namely adding the sole word
LIMITALTITUDE to the Model Checker as
an Invariant.
Running the Model Checker with Invariant
LIMITALTITUDE flagged, the software shall
produce a violation of this Invariant,
demonstrating that it is possible to reach
the limit altitude ��� in four orbits.
A HIGHERALTITUDE function shall be
implemented to demonstrate that the
spacecraft cannot reach the altitude ��� +
100 in 4 orbits.
The function name HIGHERALTITUDE
shall be in capital letters.
The HIGHERALTITUDE function shall be
coded in the Model code (i.e.: the .tla file).
The function HIGHERALTITUDE shall be
only added to the Model Checker as an
invariant, namely adding the sole word
HIGHERALTITUDE to the Model Checker
as an Invariant.
Running the Model Checker with Invariant
HIGHERALTITUDE flagged, the software
shall not produce any violation of this
Invariant, demonstrating that it is not
possible to reach the altitude ��� + 100 in
four orbits.
A comment shall be added at the end of the
code in the .tla file specifying how much is
the limiting altitude ��� found using the
invariants above.
Fig.2: The number of “Distinct States” obtained running the Model
Checker.
Fig.3: The Actions column of the Model Checking results Tab, reporting,
after running the Model Checker, all the 4 steps reported in the
requirement FORM.1
Fig.4: The occurrence of the Distinct States of the different Actions in
the Model Checking results Tab, after running the Model Checker shall
be compatible with the descending number of occurrences reported in
Specs MC.1.
PART II: Article review.
In the following, we provide a list of topics on which causality and machine
learning are related. An example of each of these topics has been
explained during the course.
- Causal Structure Discovery using Machine Learning
- Causal Generative Modelling
- Causal Explanability
- Causal Fairness
- Causal Reinforcement Learning
- Causal Computer Vision
- Causal Natural Language Processing
- Causal Graph Representation Learning
Select one of these topics, find ONE recent article related to the topic, and
write a clear and detailed explanation of its content, explaining how it
relates to concepts explained during the course, and including a critical
evaluation of it. The following instructions shall be observed:
- Specify in the title of this part which of the previous topics you chose.
- Article selection. NONE of the articles presented during the course
should be included. The selected article should be RELEVANT to the
topic. The article should NOT be a review of various articles or a survey
on the state-of-the-art in the topic, but a single independent novel piece
of research. The article should NOT be a book or a thesis. The article
should be published in a PEER-REVIEWED SCIENTIFIC JOURNAL OR
CONFERENCE. Articles from blogs, educational material, or any other
resources will not be evaluated.
- Content explanation. The description should be clear, contain the most
relevant elements of the article, and be formulated in YOUR OWN words
as much as possible. ALL technical terms that were not covered during
the lectures should be explained so as to be understood by non-experts
on the topic of the article.
- Course concepts. List ALL the concepts of the article that have been
mentioned during the course and include a very brief description of each
concept.
- Critical evaluation. Include a personal commentary that critically
evaluates some negative elements present in the article. It is not
necessary to provide an overall assessment of the article; it is sufficient to
comment in a reasoned manner on some elements of the article that are
considered negative. For example, a comment could be made on parts of
the article that are incorrect, dubious, lacking in rigour, that omit important
elements of the research, that hide or underestimate possible problems,
that present part of the work as a contribution when it is not, that is not
novel but is presented as such, that is presented as useful or impactful
when it is not, that does not consider clear negative impacts that the
research could have, etc. The reasoning should be clear, comprehensive
and adequately justified.
The critical elements should be SPECIFIC to the article, and not issues
that could be applied to any similar article.
The critical elements should NOT be mentioned already in the article.
- The bibliographic reference to the article should be included, using the
APA referencing style.
- This assignment assesses personal ability to understand, critique and
relate to previous concepts. The use of AI tools infringes its rules and will
be considered a case of academic misconduct.
- The document length for this part should be between 1 and 2 A4 pages
and should use Arial 11pt font. Any content beyond this space will NOT
be evaluated.
PART III: Directed Acyclic Graphs.
The following DAG is a partial simplified graph of a case presented during
the course:
Consider the two variables: “Ambient CO2 Level” and “Exercise”. Write all
the possible conditional independences between the two variables. I.e.
X⊥Y | A,B,C,…
Do NOT include REDUNDANT variables. E.g. If X⊥Y | A,B is true then
X⊥Y | A,B,F should not be included.
MARKING:
PART I:
The right column of Table 1 is reporting the number of points per Specs
“block”.
Each block as a pre-defined testing procedure, aiming at verifying the
corresponding Specs. Where possible, Specs are verified autonomously,
inserting the relative code in the Model Checker a running it.
PART II: Article review.
The points for this part will be distributed according to the requirements
described in the previous guidelines, and divided into two parts:
5 points. Content explanation and Course concepts.
5 points. Critical evaluation.
A total of 0 points will be awarded if the guidelines are not followed
(e.g. not a peer-reviewed single article, not relevant to the topic, not
listing and describing the concepts explained during the course,
etc.).
PART III: Directed Acyclic Graphs.
The points will be distributed uniformly between all correct
conditional independences. E.g.: If there are 10, each one will give
1 point. Each incorrect or redundant conditional independence will
subtract the same number of points.
