PHSynt

A tool for synthesizing controllers on MDPS against probabilistic hyperproperties' specifications.

PHSynt is used in

[1] "Decentralized Planning Using Probabilistic Hyperproperties". Francesco Pontiggia, Filip Macak, Roman Andriushchenko, Michele Chiari, Milan Ceska. AAMAS 2025 (a preprint is available here).

Installation

Coming soon.

Coming soon.

Name		Name	Last commit message	Last commit date
Latest commit History 1,000 Commits
.github/workflows		.github/workflows
AAMAS-experimental-models		AAMAS-experimental-models
doc/figures		doc/figures
models		models
paynt		paynt
payntbind		payntbind
tests		tests
work-in-progress-hyper-models		work-in-progress-hyper-models
.dockerignore		.dockerignore
.gitignore		.gitignore
Dockerfile		Dockerfile
LICENSE		LICENSE
README.md		README.md
install.sh		install.sh
mcbench.sh		mcbench.sh
paynt-learner.dockerfile		paynt-learner.dockerfile
paynt.py		paynt.py
paynt_pomdp_sketch.py		paynt_pomdp_sketch.py
setup.py		setup.py