Spotlight Abstraction of Agents and Areas (Extended Abstract)

Quantitative and Qualitative Analysis of Network Protocols

计算机科学;物理学

Tobe Toben1, Bernd Westphal2 and Jan-Hendrik Rakow3 ; 2 Albert-Ludwigs-Universita¨t Freiburg ; 79085 Freiburg ; Germany ; 3 Carl von Ossietzky Universita¨t Oldenburg ; 26111 Oldenburg ; Germany ; We address the problem of automatically analysing systems that vary dynam-

PID  :  82516

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

on [12] and environment abstraction [13].Let Id be a set of process identities and P a set of predicates. A system state is given by an interpretation of the predicates on the set of identities, i.e.: PIdKB (1) assigns a boolean value to each Kary predicate and Ktuple of identities. For example, unary predicates can be used to determine the current local states of processes, and binary predicates characterise the actual connection topology among processes. The behaviour of a system is then given in terms of a transition system over interpretations, that is, each state in the transition system corre sponds to one interpretation, and the transition relation determines the possible changes in the interpretations over time. A spotlight is a (typically finite) set of process identities SId. The spot light abstraction of a system state preserves the predicate interpretation of the spotlight processes S and abstracts from the rest. Formally, the abstraction transforms twovalues interpretations into threevalued interpretations S()(p, a1, . . . , an) := {