Automated circular assume-guarantee reasoning

Model checking is a successful approach for verifying hardware and software systems. Despite its success, the technique suffers from the state explosion problem which arises due to the large state space of real-life systems. One solution to the state explosion problem is compositional verification, that aims to decompose the verification of a large system into the more manageable verification of its components. To account for dependencies between components, assume-guarantee reasoning defines rules that break-up the global verification of a system into local verification of individual components, using assumptions about the rest of the system. In recent years, compositional techniques have gained significant successes following a breakthrough in the ability to automate assume-guarantee reasoning. However, automation has been restricted to simple acyclic assume-guarantee rules. In this work, we focus on automating circular assume-guarantee reasoning in which the verification of individual components mutually depends on each other. We use a sound and complete circular assume-guarantee rule and we describe how to automatically build the assumptions needed for using the rule. Our algorithm accumulates joint constraints on the assumptions based on (spurious) counterexamples obtained from checking the premises of the rule, and uses a SAT solver to synthesize minimal assumptions that satisfy these constraints. To the best of our knowledge, our work is the first to fully automate circular assume-guarantee reasoning. We implemented our approach and compared it with established non-circular compositional methods that use learning or SAT-based techniques. The experiments show that the assumptions generated for the circular rule are generally smaller, and on the larger examples, we obtain a significant speedup.     

Modular abstractions for verifying real-time distributed systems

In this work we present a verification methodology for real-time distributed systems, based on their modular decomposition into processes. Given a distributed system, each of its components is reduced by abstracting away from details that are irrelevant for the required specification. The abstract components are then composed to form an abstract system to which a model checking procedure is applied. The abstraction relation and the specification language guarantee that if the abstract system satisfies a specification, then the original system satisfies it as well.The specification languageRTL is a branching-time version of the real-time temporal logicTPTL presented in Alur and Henzinger [1]. Its model checking is linear in the size of the system and exponential in the size of the formula. Two notions of abstraction for real-time systems are introduced, each preserving a sublanguage ofRTL.     

Scalable distributed on-the-fly symbolic model checking

This paper presents a scalable method for parallel symbolic on-the-fly model checking in a distributed memory environment. Our method combines a scheme for on-the-fly model checking for safety properties with a scheme for scalable reachability analysis. We suggest an efficient, BDD-based algorithm for a distributed construction of a counterexample. The extra memory requirement for counterexample generation is evenly distributed among the processes by a memory balancing procedure. At no point during computation does the memory of a single process contain all the data. This enhances scalability. Collaboration between the parallel processes during counterexample generation reduces memory utilization for the backward step. We implemented our method on a standard, loosely- connected environment of workstations, using a high-performance model checker. Our initial performance evaluation, carried out on several large circuits, shows that our method can check models that are too large to fit in the memory of a single node. Our on-the-fly approach may find counterexamples even when the model is too large to fit in the memory of the parallel system.     

Two hemispheres—two networks: a computational model explaining hemispheric asymmetries while reading ambiguous words

A computational model for reading that takes into account the different processing abilities of the two cerebral hemispheres is presented. This dual hemispheric reading model closely follows the original computational lines due to Kowamoto (J Mem Lang 32:474–516, 1993) but postulates a difference in architecture between the right and left hemispheres. Specifically it is assumed that orthographic, phonological and semantic units are completely connected in the left hemisphere, while there are no direct connections between phonological and orthographic units in the right hemisphere. It is claimed that this architectural difference results in hemisphere asymmetries in resolving lexical ambiguity and more broadly in the processing of written words. Simulation results bear this out. First, we show that the two networks successfully simulate the time course of lexical selection in the two cerebral hemispheres. Further, we were able to see a computational advantage of two separate networks, when information is transferred from the right hemisphere network to the left hemisphere network. Finally, beyond reproducing known empirical data, this dual hemispheric reading model makes novel and surprising predictions that were found to be consistent with new human data.     

以色列卡如也特 · 比利克绿色小学—如卡弗特学校校园设计

正在学年伊始、如卡弗特学校(Rakafot School)建设完工的2周后,作为这个学校的风景园林设计师,我们接到了一个意外的电话。\"我想听听你们对于在学校‘冬日池塘’放养青蛙的意见。\"来电话的是我们的农学老师,\"我们听到了学生们对于蚊子的抱怨,因此我想,用青蛙来治理这些蚊子似乎是个不错的主意,而且青蛙的呱呱声伴随着孩子们的欢声笑语将会听起来很美妙。\"\"这听起来     

Illusion of control and behavioral control attempts in obsessive-compulsive disorder.

The present research used the illusion-of-control paradigm to examine the relationships among obsessive-compulsive disorder (OCD) symptoms, behavioral control attempts, and illusory sense of control. Participants were presented with a preprogrammed sequence of aversive and neutral visual stimuli and were encouraged to attempt to control the sequence with keyboard presses. Participants rated their perceived level of control 3 times during the task. In addition, the authors used the repetitiveness of keyboard presses as a measure of rigid, compulsive-like behavior. In Study 1, this procedure was administered to a sample of 55 students who also completed measures of OCD and depression. In Study 2, the task was administered to 22 participants with OCD and 22 matched participants without OCD. In line with predictions, OCD symptoms were correlated with higher illusory sense of control and with more repetitive behavioral control attempts. The authors discuss the central role of control in OCD and specifically the relationships between need for control and compulsive rituals, which may be conceptualized as means for achieving an illusory sense of control over stressful life events. (PsycINFO Database Record (c) 2010 APA, all rights reserved)     

Novel EIS postprocessing algorithm for breast cancer diagnosis

A new postprocessing algorithm was developed for the diagnosis of breast cancer using electrical impedance scanning. This algorithm automatically recognizes bright focal spots in the conductivity map of the breast. Moreover, this algorithm discriminates between malignant and benign/normal tissues using two main predictors: phase at 5 kHz and crossover frequency, the frequency at which the imaginary part of the admittance is at its maximum. The thresholds for these predictors were adjusted using a learning group consisting of 83 carcinomas and 378 benign cases. In addition, the algorithm was verified on an independent test group including 87 carcinomas, 153 benign cases and 356 asymptomatic cases. Biopsy was used as gold standard for determining pathology in the symptomatic cases. A sensitivity of 84% and a specificity of 52% were obtained for the test group.