Práce se zabývá problémem stavově založeného model-checkingu
Petriho sítí pro logiku větvícího se času (CTL). Petriho sítě a
formule CTL mohou být poměrně přirozeným způsobem využity pro
definování množin n-tic přirozených čísel. V práci je dokázáno,
že třída všech takovýchto množin obsahuje právě všechny množiny
definovatelné v jazyce aritmetiky (v predikátové logice prvního
řádu). V práci jsou také definovány fragmenty CTL odpovídající
jednotlivým třídám aritmetické hierarchie a pro ty je pak
dokázáno, že omezení CTL na libovolný z těchto fragmentů
omezuje třídu jimi definovatelných množin n-tic právě na
příslušnou třídu aritmetické hierarchie. Pro CTL model-checking
Petriho sítí jakožto rozhodovací problém je dokázáno, že
problém pravdivosti sentencí jazyka aritmetiky je ekvivalentně
těžký. Vedlejším výsledkem práce je důkaz rozhodnutelnosti pro
problém model-checkingu Petriho sítí a formule CTL, jejichž
negativní normální forma neobsahuje temporální operátory mimo
EF, EX a AX.