Model Checking of Computer-Based Systems

Computer-based systems, especially multi-agent systems which incorporate multi-agents physically distributed, can be represented as event structures. We propose an action-based event structure logic which is an appropriate approach specifying the action behaviors that cause states change. We discuss the symmetry of event structures. The symmetry reduction technique is used to reduce an event structures to get a simple quotient structure through the equivalence class induced by a permutation group. The action-based event structure formulas without confliction modality can be easily verified on the quotient structure for multi-agent systems