Abstract state machines: verification problems and complexity

Abstract state machines (ASMs) provide the formal foundation for a successful methodology for specification and verification of complex dynamic systems. In addition, ASMs induce a computation model on structures, which – in some sense – is more powerful and universal than the standard computation models in theoretical computer science. An investigation of ASMs is therefore interesting from both the point of view of applied computer science and the point of view of theoretical computer science. In the present thesis, practically relevant as well as theoretically motivated questions concerning ASMs are investigated. Subject of the first part of the thesis is the automatic verifiability of ASM specifications. In the second part, the ASM computation model itself and choiceless complexity classes, which have recently been defined by means of ASMs, are discussed.

Grantor dc:publisher

Publikationsserver der RWTH Aachen University

Year dc:date

2000

Author dc:creator

• Spielmann, Marc

Contributors dc:contributor

• Grädel, Erich

• info:eu-repo/classification/ddc/004
• Informatik
• Abstrakte Zustandsmaschine
• Verifikation
• Komplexitätsklasse

Statement dc:rights

• info:eu-repo/semantics/openAccess

Language dc:language

eng

Identifier

https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-123601%22

OAI identifier oai:identifier

oai:publications.rwth-aachen.de:62000