Using Semantic Tableau to Divide Model Checking Problems (IMAGE)

Japan Advanced Institute of Science and Technology

Using Semantic Tableau to Divide Model Checking Problems

Caption

Semantic tableau of a leads-to property, illustrating how conditions that must hold in current and subsequent states guide the division of the model-checking problem into smaller sub-state spaces.

Credit

Prof. Kazuhiro Ogata from JAIST. Image Source Link: https://doi.org/10.1145/3836770

Usage Restrictions

Credit must be given to the creator.

License

CC BY

Disclaimer: AAAS and EurekAlert! are not responsible for the accuracy of news releases posted to EurekAlert! by contributing institutions or for the use of any information through the EurekAlert system.