Login

Recent searches

No recent searches

Search options

Not available on mastodon.xyz.
mastodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance, open to everyone, but mainly English and French speaking.

Administered by:

Server stats:

714
active users

mastodon.xyz: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.4

#IsabelleHOL

4 posts4 participants0 posts today
Public
José A. Alonso

Formally verified certification of unsolvability of temporal planning problems. ~ David Wang, Mohammad Abdulaziz. arxiv.org/abs/2510.10189 #ITP #IsabelleHOL

arXiv logo
arXiv.orgFormally Verified Certification of Unsolvability of Temporal Planning ProblemsWe present an approach to unsolvability certification of temporal planning. Our approach is based on encoding the planning problem into a network of timed automata, and then using an efficient model checker on the network followed by a certificate checker to certify the output of the model checker. Our approach prioritises trustworthiness of the certification: we formally verify our implementation of the encoding to timed automata using the theorem prover Isabelle/HOL and we use an existing certificate checker (also formally verified in Isabelle/HOL) to certify the model checking result.
Public
José A. Alonso

Formally verified certification of unsolvability of temporal planning problems. ~ David Wang, Mohammad Abdulaziz. arxiv.org/abs/2510.10189 #ITP #IsabelleHOL

arXiv logo
arXiv.orgFormally Verified Certification of Unsolvability of Temporal Planning ProblemsWe present an approach to unsolvability certification of temporal planning. Our approach is based on encoding the planning problem into a network of timed automata, and then using an efficient model checker on the network followed by a certificate checker to certify the output of the model checker. Our approach prioritises trustworthiness of the certification: we formally verify our implementation of the encoding to timed automata using the theorem prover Isabelle/HOL and we use an existing certificate checker (also formally verified in Isabelle/HOL) to certify the model checking result.
ExploreLive feeds
About