Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: Kripke semantics

Sortuj według:

Ogranicz wyniki do:

Parameter Synthesis for Timed Kripke Structures

Knapik M., Penczek W.

Fundamenta Informaticae

2014

Vol. 133, nr 2/3

211--226

We show how to synthesise parameter values under which a given property, expressed in a certain extension of CTL, called RTCTLP, holds in a parametric timed Kripke structure. We prove the decidability of parameter synthesis for RTCTLP by showing how to restrict the infinite space of parameter valuations to its finite subset and employ a brute-force algorithm. The bruteforce approach soon becomes intractable, therefore we propose a symbolic algorithm for RTCTLP parameter synthesis. Similarly to the fixed-point symbolic model checking approach, we introduce special operators which stabilise on the solution. The process of stabilisation is essentially a translation from the RTCTLP parameter synthesis problem to a discrete optimization task. We show that the proposedmethod is sound and complete and provide some complexity results. We argue that this approach leads to new opportunities in model checking, including the use of integer programming and related tools.

A Tuning Machine for Cooperative Problem Solving

Dunin-Kęplicz B., Verbrugge R.

Fundamenta Informaticae

2004

Vol. 63, nr 2,3

283--307

In this paper we aim to formally model individual, social and collective motivational attitudes in teams of agents involved in Cooperative Problem Solving. Particular attention is given to the strongest motivational attitude, collective commitment, which leads to team action. First, building on our previous work, a logical framework is sketched in which social commitments and collective intentions are formalized. Then, different versions of collective commitments are given, reflecting different aspects of Cooperative Problem Solving, and applicable in different situations. The definitions differ with respect to the aspects of teamwork of which the agents involved are aware, and the kind of awareness present within a team. In this way a kind of tuning mechanism is provided for the system developer to tune a version of collective commitment fitting the circumstances. Finally, we focus attention on a few exemplar versions of collective commitment resulting from instantiating the general tuning scheme, and sketch for which kinds of organization and application domains they are appropriate.