The design of a complex system warrants a compositional methodology, i.e., composing simple components to obtain a larger system that exhibits their collective behavior in a meaningful way. We propose an automaton-based paradigm for compositional design of such systems where an action is accompanied by one or more preferences. At run-time, these preferences provide a natural fallback mechanism for the component, while at design-time they can be used to reason about the behavior of the component in an uncertain physical world. Using structures that tell us how to compose preferences and actions, we can compose formal representations of individual components or agents to obtain a representation of the composed system. We extend Linear Temporal Logic with two unary connectives that reflect the compositional structure of the actions, and show how it can be used to diagnose undesired behavior by tracing the falsification of a specification back to one or more culpable components.
The automata formalism used in this paper generalizes @cite_26 @cite_4 . The latter were originally proposed to give descriptions of Web Services @cite_4 ; in @cite_32 , they were used to model fault-tolerant, compositional autonomous agents. Using preference values to specify the behavior of autonomous agents is also explored from the perspective of rewriting logic in the @cite_31 @cite_18 . Recent experiments with the Soft Agent Framework show that behavior based on soft constraints can indeed contribute robustness @cite_12 .
@cite_18 @cite_26 @cite_4 @cite_32 @cite_31 @cite_12
2160106331 2962845465 1665497870 71507039
Abstract We present an approximation technique, that can render real-time model checking of safety and universal path properties more efficient. It is beneficial, when loops lead to repetition of control situations. Basically we augment a timed automata model with carefully selected extra transitions. This increases the size of the state-space, but potentially decreases the number of symbolic states to be explored by orders of magnitude. We give a formal definition of a timed automata formalism, enriched with basic data types, hand-shake synchronization, urgency, and committed locations. We prove by means of a trace semantics, that if a safety property can be established in the augmented model, it also holds for the original model. We extend our technique to a richer set of properties, that can be decided via a set of traces (universal path properties). In order for universal path properties to carry over to the original model, the semantics of the timed automata formalism is formulated relative to the applied augmentation. Our technique is particularly useful in systems, where a scheduler dictates repetition of control over elapsing time. As a typical example we mention translations of LEGO® RCX™ programs to U ppaal models, where the Round-Robin scheduler is a static entity. We allow scheduler and associated tasks to “park”, until some timing or environmental conditions are met. We apply our technique on a brick-sorter model for a safety property and report run-time data. The paper presents a knowledge representation formalism, in the form of a high-level Action Description Language (ADL) for multi-agent systems, where autonomous agents reason and act in a shared environment. Agents are autonomously pursuing individual goals, but are capable of interacting through a shared knowledge repository. In their interactions through shared portions of the world, the agents deal with problems of synchronization and concurrency; the action language allows the description of strategies to ensure a consistent global execution of the agents’ autonomously derived plans. A distributed planning problem is formalized by providing the declarative specications of the portion of the problem pertaining a single agent. Each of these specications is executable by a stand-alone CLP-based planner. The coordination among agents exploits a Linda infrastructure. The proposal is validated in a prototype implementation developed in SICStus Prolog. To appear in Theory and Practice of Logic Programming (TPLP). Research partially funded by GNCS-INdAM projects, MUR-PRIN: Innovative and multidisciplinary approaches for constraint and preference reasoning project; NSF grants IIS-0812267 and HRD-0420407; and grants 2009.010.0336 and 2010.011.0403. We extend Constraint Automata by replacing boolean constraints with semiring-based soft constraints. The obtained general formal tool can be used to represent preference-based and similarity-based queries, which allow a user more freedom in choosing the behavior of the service to finally use, among all possible choices. A user states his preferences through a “soft” query, and obtains results that satisfy this query with different levels of preference. The soft requirements may involve a parameter data of the service operations, or the (names of the) operations themselves. Moreover, we introduce a first implementation of the search procedure by using declarative (soft) Constraint Programming. We are interested in principles for designing and building open distributed systems consisting of multiple cyber-physical agents, specifically, where a coherent global view is unattainable and timely consensus is impossible. Such agents attempt to contribute to a system goal by making local decisions to sense and effect their environment based on local information. In this paper we propose a model, formalized in the Maude rewriting logic system, that allows experimenting with and reasoning about designs of such systems. Features of the model include communication via sharing of partially ordered knowledge, making explicit the physical state as well as the cyber perception of this state, and the use of a notion of soft constraints developed by Martin Wirsing and his team to specify agent behavior. The paper begins with a discussion of desiderata for such models and concludes with a small case study to illustrate the use of the modeling framework.