Cílem projektu je výzkum problémů týkajících se nekonečně-stavových pravděpodobnostních systémů, především otázek rozhodnutelnosti a algoritmické složitosti. Doposud zkoumané pravděpodobnostní systémy byly pouze konečně-stavové, avšak řada reálných systémů používá struktury s neomezenou velikostí. Projekt si klade za cíl posunout možnosti formální verifikace na nekonečně-stavové pravděpodobnostní systémy, což vyžaduje řešení těžkých kombinatorických problémů z oblasti Markovových řetězců a nekonečných grafů. V mnoha případech nelze adaptovat existující metody a přístupy a je třeba hledat nové.