English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

This paper is concerned with developing a software tool, called IMPaCT, forthe parallelized verification and controller synthesis of large-scalestochastic systems using interval Markov chains (IMCs) and interval Markovdecision processes (IMDPs), respectively. The tool serves to (i) constructIMCs/IMDPs as finite abstractions of underlying original systems, and (ii)leverage interval iteration algorithms for formal verification and controllersynthesis over infinite-horizon properties, including safety, reachability, andreach-avoid, while offering convergence guarantees. IMPaCT is developed in C++and designed using AdaptiveCpp, an independent open-source implementation ofSYCL, for adaptive parallelism over CPUs and GPUs of all hardware vendors,including Intel and NVIDIA. IMPaCT stands as the first software tool for theparallel construction of IMCs/IMDPs, empowered with the capability to leveragehigh-performance computing platforms and cloud computing services.Specifically, parallelism offered by IMPaCT effectively addresses thechallenges arising from the state-explosion problem inherent indiscretization-based techniques applied to large-scale stochastic systems. Webenchmark IMPaCT on several physical case studies, adopted from the ARCH toolcompetition for stochastic models, including a 2-dimensional robot, a3-dimensional autonomous vehicle, a 5-dimensional room temperature system, anda 7-dimensional building automation system. To show the scalability of ourtool, we also employ IMPaCT for the formal analysis of a 14-dimensional casestudy.

IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale Stochastic Systems