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...     

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.     

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.     

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)     

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.     

The Adsorption of Pollutants by Peat,Lignite and Activated Chars

The ability of peat, lignite and activated chars made from peat and lignite to adsorb dyes and metals from wastewater and NO₂ from air was investigated. Equilibrium isotherms were determined to assess the maximum adsorption capacity of the adsorbents for the pollutants. Kinetic studies for the adsorption of dyes and metal ions onto the adsorbents were undertaken in agitated batch adsorbers. Mass transport models were tested to predict the concentration decay curves in batch adsorbers. The models tested were single resistance models based on the assumption of a single external mass transfer coefficient and two resistance models which included an internal diffusion coefficient and an external mass transfer coefficient. The surface phenomena which influence the extent and the rate of uptake have been studied. The equilibrium capacity data conform to Langmuir plots. A previously proposed model was used to evaluate the external single resistance mass transfer model and was successfully applied to predict the adsorption of metal ions in single component systems under batch conditions. It has been shown that the assumption of negligible intraparticle diffusion is valid and that external film diffusion is the rate limiting step in describing the adsorption processes at high sorbent loadings. The same type of result is not observed for the adsorption of coloured organic matter onto peat where the sorption processes cannot be successfully modelled by use of a single resistance model and a two resistance model incorporating internal diffusion is required. The surface phenomena which influence the extent and the rate of uptake of NO₂ have been studied. The type of chars produced and the activation processes affect the adsorption. As activation increases, micropore volume and surface area increase and the maximum capacity of the adsorbent increases. Surface area alone is not the only parameter which affects equilibrium uptake. © 1997 SCI.     

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.     

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