Spousal support and cardiac patients' distress: The moderating role of attachment orientation.

Based on the Person–Environment Fit Model, the current prospective study explored the contribution of the interaction between spouses' ways of providing support and patients' attachment orientations to the patients' levels of psychological distress 6 months after experiencing a first Acute Coronary Syndrome (ACS). One hundred and eleven patients completed a measure of attachment orientations during hospitalization, while their spouses completed a measure of ways of providing support 1 month later. The outcome measures were patients' depressive and anxiety symptoms 6 months after their ACS. Whereas active engagement was associated with lower levels of anxiety symptoms among patients high in attachment anxiety, it was also associated with higher levels of anxiety symptoms among patients low on this orientation. In addition, none of the ways of providing support moderated the association between avoidance and distress. These results shed light on the possible interplay between providers' support and recipients' personalities. (PsycINFO Database Record (c) 2010 APA, all rights reserved)     

A work-efficient distributed algorithm for reachability analysis

This work presents a novel distributed symbolic algorithm for reachability analysis that can effectively exploit, as needed, a large number of machines working in parallel. The novelty of the algorithm is in its dynamic allocation and reallocation of processes to tasks and in its mechanism for recovery from local state explosion. As a result, the algorithm is work-efficient: it utilizes only those resources that are actually needed. In addition, its high adaptability makes it suitable for exploiting the resources of very large and heterogeneous distributed, nondedicated environments. Thus, it suitable for verifying very large systems. We implemented our algorithm in a tool called Division. Our experimental results show that the algorithm is indeed work-efficient. Although the goal of this research is to check larger models, the results also indicate that the algorithm can obtain high speedups, because communication overhead is very small.     

Preface: Volume 68 Issue 4

This issue contains the Proceedings of the First International Workshop on Parallel and Distributed Model Checking (PDMC 2002) held in Brno, Czech Republic, August 19, 2002 as a satellite event to the 13th International Conference on Concurrency Theory (CONCUR 2002).The aim of the PDMC 2002 workshop was to cover all aspects of parallel and distributed model checking and supporting techniques. The mission was on one side to introduce people to the field of parallel and distributed model checking and on the other side to be a working forum for describing new research building thus the relationship between people working in the area of parallel and distributed approaches to the verification of large-scale systems and to encourage cross-fertilization of ideas.The workshop programme consisted of:

2 invited talks, respectively by Moshe Vardi on Model Checking: A Complexity-Theoretic Perspective and by Orna Grumberg on Different directions in parallel and distributed model checking,

8 regular presentations, and

5 short presentations.

The proceedings contains the regular papersonly. The regular papers and short presentations have been accepted by the following programme committee:

Lubos Brim (MU Brno, Czech Republic) - Co-chair

Gianpiero Cabodi (Torino, Italy)

Hubert Garavel (INRIA, France)

Orna Grumberg (Technion, Israel) - Co-chair

Boudewijn R. Haverkort (Aachen, Germany)

Kim Larsen (BRICS Aalborg, Denmark)

Rajeev Ranjan (Real Intent, USA)

We would like to thank very much to all members of the programme committee for nice cooperation and for detailed reports and comments and to all the authors for their contributions. For online-information see http://www.fi.muni.cz/concur2002/PDMC/.

August 19, 2002	Lubos Brim
	Orna Grumberg

Full-size table

     

Static Analysis for State-Space Reductions Preserving Temporal Logics

In this paper we present two methods that use static analysis of parallel programs to create reduced models for them. Our algorithms examine the control-flow graph of a program (the syntax) and create a smaller transition system than would have been created otherwise. The smaller transition system is equivalent to the original transition system of the program with respect to temporal logic specifications.The two methods are orthogonal in their approach. The first, called path reduction, reduces the state-space by compressing computation paths. This method reduces the number of steps each computation takes. The second method, called dead variable reduction, reduces according to the variable domains. It identifies classes of equivalent states which differ only on variable values (and not the program counter) and uses a representative for each class. We also consider a refinement of the dead variable reduction, based on partially dead variables, which may result in a greater reduction.Our algorithms are based on syntactic manipulation of expressions, thus enabling us to handle programs with variables over finite as well as infinite domains. Both methods can easily be combined with either explicit state or symbolic methods (and with each other).We used the Murphi verifier to test the amount of reduction achieved by both methods. We let Murphi perform a DFS search and compared the sizes of the original and reduced transition systems, for several examples and according to both reductions. The results show that path reduction and the reduction based on partially dead variables give significant reductions, while the effect of fully dead variables is less impressive. We discuss the differences between the approaches, and the reasons for these results.     

From liveness to promptness

Liveness temporal properties state that something “good” eventually happens, e.g., every request is eventually granted. In Linear Temporal Logic (LTL), there is no a priori bound on the “wait time” for an eventuality to be fulfilled. That is, F θ asserts that θ holds eventually, but there is no bound on the time when θ will hold. This is troubling, as designers tend to interpret an eventuality F θ as an abstraction of a bounded eventuality F ^≤k θ, for an unknown k, and satisfaction of a liveness property is often not acceptable unless we can bound its wait time. We introduce here prompt-LTL, an extension of LTL with the prompt-eventually operator F _p . A system S satisfies a prompt-LTL formula φ if there is some bound k on the wait time for all prompt-eventually subformulas of φ in all computations of S. We study various problems related to prompt-LTL, including realizability, model checking, and assume-guarantee model checking, and show that they can be solved by techniques that are quite close to the standard techniques for LTL.     

Certifying DFA Bounds for Recognition and Separation

Innovations in Systems and Software Engineering - The automation of decision procedures makes certification essential. We suggest to use determinacy of turn-based two-player games with regular...     

STRATEGIC NEGOTIATION FOR SHARING A RESOURCE BETWEEN TWO AGENTS*

In this article, we propose a strategic negotiation model that enables self‐motivated rational agents to share resources. The strategic negotiation model takes the passage of time during the negotiation process itself into account. The model considers bilateral negotiations in situations characterized by complete information, in which one agent loses over time whereas the other gains over time. Using this negotiation mechanism, autonomous agents apply simple and stable negotiation strategies that result in efficient agreements without delay, even when there are dynamic changes in the environment. Simulation results show that our mechanism performs as well as a centralized scheduler and also has the property of balancing the resources' usage.     

Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking

This work presents a collection of methods that integrate symmetry reduction and under-approximation with symbolic model checking in order to reduce space and time. The main objective of these methods is falsification. However, under certain conditions, they can provide verification as well.We first present algorithms that use symmetry reduction to perform on-the-fly model checking for temporal safety properties. These algorithms avoid building the orbit relation and choose representatives on-the-fly while computing the reachable states. We then extend these algorithms to check liveness properties as well. In addition, we introduce an iterative on-the-fly algorithm that builds subsets of the orbit relation rather than the full relation.Our methods are fully automatic once the user supplies some basic information about the symmetry in the verified system. Moreover, the methods are robust and work correctly even if the information supplied by the user is incorrect. Furthermore, the methods return correct results even when the computation of the symmetry reduction has not been completed due to memory or time explosion.We implemented our methods within the IBM model checker Rule-Base and compared their performance to that of RuleBase. In most cases, our algorithms outperformed RuleBase in both time and space.