Compact Representations and Efficient Algorithms for Operating Guidelines

Abstract

Operating guidelines characterize correct interaction (e. g., deadlock freedom) with a service. They can be stored in a service registry. They are typically represented as an annotated transition system where the annotations are Boolean formulae atta