L*_sha: L*-Based Algorithm for Stochastic Hybrid Automata Learning

This repository contains the implementation of L*_sha, an algorithm to learn Stochastic Hybrid Automata from collected system traces. The algorithm is not tied to a specific domain, although it has been successfully exploited to infer a model of human behavior in human-robot interaction scenarios building upon the work presented in:

• Formal Modeling and Verification of Multi-Robot Interactive Scenarios in Service Settings
• A Deployment Framework for Formally Verified Human-Robot Interactions
• A Model-driven Approach for the Formal Analysis of Human-Robot Interaction Scenarios
• Formal Verification of Human-Robot Interaction in Healthcare Scenarios
• Statistical Model Checking of Human-Robot Interaction Scenarios

The algorithm builds upon L*, whose main elements are:

• a Teacher that stores the collected traces and answers queries based on currently accumulated knowledge
• a Learner that progressively refines the hypothesis automaton by asking queries to the Teacher

The teacher relies on samples of the System Under Learning (SUL) (i.e., it does not possess exact knowledge). To generate traces for the specific use case of human-robot interaction, we exploit either Uppaal with manually drafted SHA to be learned or the deployment framework to simulate the robotic application in a virtual environment and collect the simulation traces.

Authors:

Learned SHA

Learned SHA for the thermostat case study can be found here.

Learned SHA for the human-robot interaction case study can be found here.

Configuration File Setup

The main L*_sha script requires as input parameter the path to a configuration file, whose template can be found within the ./resources/config/ folder.

Make sure to set each property to match your environment, specifically:

• N_min is the minimum number of observations for each trace to stop perfoming the refinement query (i.e., a value greater than 10 is advised);
• CASE_STUDY is the chosen SUL (either THERMO or HRI);
• CS_VERSION is the experiment you want to perform for the chosen SUL;
• RESAMPLE_STRATEGY is the chosen approach to generate new SUL traces (either UPPAAL or SIM).

If the chosen resample strategy is UPPAAL:

• UPPAAL_PATH is the path to Uppaal command line utility;
• UPPAAL_SCRIPT_PATH is the path to verify.sh;
• UPPAAL_MODEL_PATH is the path to the Uppaal model template (e.g., hri-w_ref.xml);
• UPPAAL_QUERY_PATH is the path to the Uppal query template (e.g., thermostat.q);
• UPPAAL_OUT_PATH is the path where you want the generated traces to be stored.

If the chosen resample strategy is SIM:

• SIM_LOGS_PATH is the path to available SUL traces.

Note: The algorithm has been tested on Uppaal v.4.1.24 on Mac OS X. Should you run into any issue while testing with a different configuration please report to livia.lestingi@polimi.it.

Python Dependencies

Install the required dependencies:

pip install -r $LSHA_REPO_PATH/requirements.txt

Add the L*_SHA repo path to your Pytho path (fixes ModuleNotFoundError while trying to execute from command line):

export PYTHONPATH="${PYTHONPATH}:$LSHA_REPO_PATH"

Run the main script specifying the path to your configuration file:

python3 $LSHA_REPO_PATH/it/polimi/hri_learn/learn_model.py $CONFIG_FILE_PATH

Copyright © 2021 Livia Lestingi