Skip to content

Learning parameter documentation #51

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
mikucionisaau wants to merge 4 commits into
base: main
Choose a base branch
from
Draft

Learning parameter documentation #51

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9c767c2
Started documenting learning parameters
mikucionisaau Jan 19, 2024
a1fe825
Added learning parameter description
mikucionisaau Sep 20, 2024
eeb0bc4
Merge remote-tracking branch 'gh/learning-params' into learning
mikucionisaau Sep 20, 2024
4c97ddd
Cleanup learning parameters
mikucionisaau Oct 17, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
90 changes: 85 additions & 5 deletions content/gui-reference/menu-bar/options.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -105,12 +105,8 @@ Adjusts the amount of memory used to represent the state space when using bit-st

When selected, instructs the verifier to (whenever possible) reuse the generated portion of the state space when several properties of the same system are checked.

<a name="statparam">

## Statistical Parameters

</a>

Lower probabilistic deviation (-δ)
: Used in hypothesis testing (qualitative model-checking) to specify the lower bound of indifference region from the specified probability.

Expand Down Expand Up @@ -139,8 +135,92 @@ Histogram bucket count
: Specifies the number of columns in the histogram. By default it is set to zero meaning that the count is determined by taking a square root of a total number of samples and dividing by four.


## Learning Parameters

Based on publication: [On Time with Minimal Expected Cost!](https://homes.cs.aau.dk/~kgl/SSFT2015/ATVA.pdf) (Fig.2).

Discussion: [Way to set a fixed number of training runs for reinforcement learning](https://github.com/orgs/UPPAALModelChecker/discussions/232#discussioncomment-8153813)

Learning filter:
- `Global filter`
- `Local filter`
- `Sweep filter`

Learning method
- `External learning library`
- `Co-variance`
- `Splitting`
- `Regression`
- `Naive`
- `Q-learning`
- `M-learning`

Number of successful runs
:

Maximum number of runs
:

Number of good runs
:

Number of runs to evaluate
:

Total maximal number of iterations
:

Imitation iterations
:

Iterations with no improvement before reset
:

Maximum number of resets
:

Learning rate for Q-Learning
:

Upper limit for T-Test
:

Lower limit for T-Test
:

Limit for KS-Split
:

Filter smoothing
:

Critical filter value
:

Learning discount
:

Stochastic runs (%)
:

Deterministic runs (%)
:

Critical difference (%)
:

Difference smoothing (runs)
:


## More Information

Learning algorithm and parameters are described in the following papers:

- [ATVA2019] _Teaching Stratego to Play Ball: Optimal Synthesis for Continuous Space MDPs_, Manfred Jaeger, Peter Gjøl Jensen, Kim Guldstrand Larsen, Axel Legay, Sean Sedwards & Jakob Haahr Taankvist. In: Chen, YF., Cheng, CH., Esparza, J. (eds) Automated Technology for Verification and Analysis. ATVA 2019. Lecture Notes in Computer Science(), vol 11781. Springer, Cham. [doi:10.1007/978-3-030-31784-3_5](https://doi.org/10.1007/978-3-030-31784-3_5)

- [ATVA2015] _On Time with Minimal Expected Cost!_, Alexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Axel Legay, Didier Lime, Mathias Grund Sørensen and Jakob H. Taankvist. In: Cassez, F., Raskin, JF. (eds) Automated Technology for Verification and Analysis. ATVA 2014. Lecture Notes in Computer Science, vol 8837. Springer, Cham. [doi:10.1007/978-3-319-11936-6_10](https://doi.org/10.1007/978-3-319-11936-6_10)

The compact data structure and the options for state space reduction are described in the following paper:

> _Efficient Verification of Real-Time Systems: Compact Data Structure and State Space Reduction_, Kim G. Larsen, Fredrik Larsson, Paul Pettersson and Wang Yi. In Proceedings of the 18th IEEE Real-Time Systems Symposium, pages 14-24\. San Francisco, California, USA, 3-5 December 1997.
- [RTSS1997] _Efficient Verification of Real-Time Systems: Compact Data Structure and State Space Reduction_, Kim G. Larsen, Fredrik Larsson, Paul Pettersson and Wang Yi. In Proceedings of the 18th IEEE Real-Time Systems Symposium, pages 14-24. San Francisco, California, USA, 3-5 December 1997. [doi:10.1109/REAL.1997.641265](https://doi.org/10.1109/REAL.1997.641265)
2 changes: 1 addition & 1 deletion content/language-reference/query-syntax/learning_queries.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,4 +54,4 @@ Integers, clocks, floating points or even arbitrary expressions can be used in e
Process locations are ignored when specifying observability unless explicitly specified using `location` keyword.
For example `Cat.location` and `Mouse.location` refer to the locations of `Cat` and `Mouse` processes.

The learning queries are usually used together with strategy assignment and refinement explained in [Strategy Queries]({{<relref "/strategy_queries">}}).
The learning queries are usually used together with strategy assignment and refinement explained in [Strategy Queries]({{<relref "strategy_queries">}}).