engleski

Progressing Collaborative Systems

This paper builds on existing models for collaborative systems with confidentiality policies. The actions in these models are balanced, namely, they have an equal number of facts in their pre- and post-conditions. Here we consider a further restriction that each instance of an action is used at most once in a process. Administrative processes usually involve such progressing behavior, that is, whenever a transaction is performed, it does not need to be repeated. We investigate the complexity of the decision problem whether there exists a sequence of transitions from an initial state to a final state that avoids any critical states, e.g., states which conflict with the given confidentiality policies. We show that this problem is NP-complete when balanced actions do not involve fresh values and when the system is progressing. The same problem is shown to be PSPACE-complete when the system is not progressing, and PSPACE-hard when the system is progressing, but when actions may update values with fresh ones. The bounds hold even when balanced actions change only one fact in a configuration. We implement some examples in logic-based verification tools and model-check that they comply with certain policies.

collaborative systems; critical configurations; policy compliance; multiset rewriting; complexity; model checking; linear logic

http://www.math.uniri.hr/NATO-ASI/