pHL-PR/1.3 — Hybrid Language (Probabilistic Reasoning)

Type:package
State:under development and/or testing
Servers:vm2, vm1

About

pHL-PR is just the container and sDL interface of the software ProbReach [2], which is a tool [1] for calculating bounded probabilistic reachability and performing parameter set synthesis in hybrid systems with uncertainty in initial parameters. pHL-PR supports formal verification (computing rigorous enclosures) and statistical model checking (Chernoff-Hoeffding bound and Bayesian estimations).

sDL structure

Follows the standard sDL structure:

//%SCOPE description text

#include "somefile"

BEGIN-CODE [ pHL-PR/1.3 | {package options} ]
{package commands}
END-CODE

Commented lines, in the CODE body text, start with “##”.

Namespaces and commands

The standard “core” namespace is available.

Folders

(information will be added later by the package administrator)

References

[1]
  1. Shmarov and P. Zuliani, ProbReach: Verified Probabilistic Delta-Reachability for Stochastic Hybrid Systems (arxiv)
[2]ProbReach (website)

Change Log

Version 1.3

2016/09/21 - Added package to sDL

(Documentation updated on 2018-12-31 12:15)