Präsentation der Master-Thesis von Amin Timany
20.6.2013, 9:30 Uhr, INF 3027
Model checking is an automated approach to verification of systems, e.g., software systems, hardware systems, communication protocols, etc. This is done via representing the system as a transition system, that is, representing different situations that the system can be in as a number of states and their relations, while representing properties that have to be verified as temporal logic formulas. Unfortunately, when the system at hand is comprised of a number of sub-systems (processes or components) that run in parallel, the number of states of the system grows exponentially in the number of sub-systems that run in parallel. For tackling this phenomenon, called state space explosion problem, there have been several approaches developed. A well known and widely practiced approach is symmetry reduction that makes use of symmetry of sub-systems running in parallel to reduce the number of states of the composite system.