Základné crty teórie, ktorú budeme pouzívat:
Nedeterminizmus (je to jednoduchšie s ním a postupným zjemnením môze byt odstránený); niektoré systémy sú zo svojej povahy nedeterministické, napr. OS
synchrónnost a asynchrónnost
stavy a priradenia (prechodové systémy)
kód programu nie je prepletený s dôkazom
správnost (závisí len od programu) a zlozitost (závisí od programu a jeho implementácie na konkrétnej architektúre) sú oddelené