Evrostos

Evrostos

Description: Evrostos is a model-checking tool for Robust Linear-time Temporal Logic (rLTL). The logic, rLTL, was crafted to embed the notion of robustness into LTL. The main advantages of rLTL are:

1. It can express the notion of robustness in reactive specifications, whereas LTL cannot.
2. rLTL is a 5-valued logic, that provides more fine-grained information when a specification is violated, and not just false.

Therefore, rLTL verification provides much more insight than classical LTL verification. For more details on this, see our paper Evrostos: The rLTL Verifier.

VO Integration: No

Active: Yes

Available Benchmarks: No

Website: GitHub repository.

Download: See repository for code and installation instructions.

Documentation: See readme and examples in repository. There is also the tool paper mentioned above.

Contact: Tzanis Anevlavis (see paper for email)

Excerpt from: https://github.com/janis10/evrostos