scholarly journals Models of Concurrent Kleene Algebra

10.29007/qp92 ◽  
2020 ◽  
Author(s):  
Alexandra Silva
Keyword(s):  
Concurrent Programs ◽  
Sequential Consistency ◽  
Partial Observations ◽  
Control Structures ◽  
Kleene Algebra ◽  
Ongoing Work ◽  
Algebraic Framework ◽  
Memory Accesses ◽  
The Right ◽  
Partially Observable

Kleene Algebra and variants thereof have been successfully used in verification of se- quential programs. The leap to concurrent programs offers many challenges, both in terms of devising the right foundations to study concurrent variants of Kleene Algebra but also in finding the right models to enable effective verification of relevant programs. In this talk, we will review existing and ongoing work on concurrent Kleene Algebra with a focus on a variant called partially observable concurrent Kleene algebra (POCKA). POCKA offers an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. We will show how a previously developed technique for com- pleteness of Kleene Algebra can be lifted to prove that POCKA is a sound and complete axiomatization of a model of partial observations. We illustrate the use of the framework in the analysis of sequential consistency, i.e., whether programs behave as if memory accesses taking place were interleaved and executed sequentially.The work described in this invited talk is based on [1, 2, 3], and it is joint with a won- derful group of people: Paul Brunet, Simon Docherty, Tobias Kapp ́e, Jurriaan Rot, Jana Wagemaker, and Fabio Zanasi.

scholarly journals Attentional Preparation for a Lateralized Visual Distractor: Behavioral and fMRI Evidence

2006 ◽  
Vol 18 (4) ◽  
pp. 522-538 ◽  
Author(s):  
Christian C. Ruff ◽  
Jon Driver
Keyword(s):  
Occipital Cortex ◽  
Brain Structures ◽  
Functional Coupling ◽  
Psychophysical Experiment ◽  
Temporoparietal Junction ◽  
Control Structures ◽  
Visual Distractor ◽  
Superior Parietal Cortex ◽  
The Right ◽  
The Impact

Attending to the location of an expected visual target can lead to anticipatory activations in spatiotopic occipital cortex, emerging before target onset. But less is known about how the brain may prepare for a distractor at a known location remote from the target. In a psychophysical experiment, we found that trial-to-trial advance knowledge about the presence of a distractor in the target-opposite hemifield significantly reduced its behavioral cost. In a subsequent functional magnetic resonance imaging experiment with similar task and stimuli, we found anticipatory activations in the occipital cortex contralateral to the expected distractor, but no additional target modulation, when participants were given advance information about a distractor's subsequent presence and location. Several attention-related control structures (frontal eye fields and superior parietal cortex) were active during attentional preparation for all trials, whereas the left superior prefrontal and right angular gyri were additionally activated when a distractor was anticipated. The right temporoparietal junction showed stronger functional coupling with occipital regions during preparation for trials with an isolated target than for trials with a distractor expected. These results show that anticipation of a visual distractor at a known location, remote from the target, can lead to (1) a reduction in the behavioral cost of that distractor, (2) preparatory modulation of the occipital cortex contralateral to the location of the expected distractor, and (3) anticipatory activation of distinct parietal and frontal brain structures. These findings indicate that specific components of preparatory visual attention may be devoted to minimizing the impact of distractors, not just to enhancements of target processing.

A Generic Approach to the Static Analysis of Concurrent Programs with Procedures

2003 ◽  
Vol 14 (04) ◽  
pp. 551-582 ◽  
Author(s):  
Ahmed Bouajjani ◽  
Javier Esparza ◽  
Tayssir Touili
Keyword(s):  
Static Analysis ◽  
Concurrent Programs ◽  
Finite Chain ◽  
Algebraic Framework ◽  
Emptiness Problem ◽  
Model Programs ◽  
Context Free

We present a generic aproach to the static analysis of concurrent programs with procedures. We model programs as communicating pushdown systems. It is known that typical dataflow problems for this model are undecidable, because the emptiness problem for the intersection of context-free languages, which is undecidable, can be reduced to them. In this paper we propose an algebraic framework for defining abstractions (upper approximations) of context-free languages. We consider two classes of abstractions: finite-chain abstractions, which are abstractions whose domains do not contain any infinite chains, and commutative abstractions corresponding to classes of languages that contain a word if and only if they contain all its permutations. We show how to compute such approximations by combining automata theoretic techniques with algorithms for solving systems of polynomial inequations in Kleene algebras.

scholarly journals Learning Partially Observable Deterministic Action Models

2008 ◽  
Vol 33 ◽  
pp. 349-402 ◽  
Author(s):  
E. Amir ◽  
A. Chang
Keyword(s):  
Reinforcement Learning ◽  
Logical Structure ◽  
Exact Algorithms ◽  
Ai Planning ◽  
Partial Observations ◽  
Domain Structures ◽  
Action Model ◽  
Action Models ◽  
Partially Observable ◽  
Over Time

We present exact algorithms for identifying deterministic-actions' effects and preconditions in dynamic partially observable domains. They apply when one does not know the action model(the way actions affect the world) of a domain and must learn it from partial observations over time. Such scenarios are common in real world applications. They are challenging for AI tasks because traditional domain structures that underly tractability (e.g., conditional independence) fail there (e.g., world features become correlated). Our work departs from traditional assumptions about partial observations and action models. In particular, it focuses on problems in which actions are deterministic of simple logical structure and observation models have all features observed with some frequency. We yield tractable algorithms for the modified problem for such domains. Our algorithms take sequences of partial observations over time as input, and output deterministic action models that could have lead to those observations. The algorithms output all or one of those models (depending on our choice), and are exact in that no model is misclassified given the observations. Our algorithms take polynomial time in the number of time steps and state features for some traditional action classes examined in the AI-planning literature, e.g., STRIPS actions. In contrast, traditional approaches for HMMs and Reinforcement Learning are inexact and exponentially intractable for such domains. Our experiments verify the theoretical tractability guarantees, and show that we identify action models exactly. Several applications in planning, autonomous exploration, and adventure-game playing already use these results. They are also promising for probabilistic settings, partially observable reinforcement learning, and diagnosis.

scholarly journals Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness

2020 ◽  
pp. 381-400
Author(s):  
Tobias Kappé ◽  
Paul Brunet ◽  
Alexandra Silva ◽  
Jana Wagemaker ◽  
Fabio Zanasi
Keyword(s):  
Composition Operator ◽  
Completeness Theorem ◽  
Independent Interest ◽  
Concurrent Programs ◽  
Parallel Composition ◽  
General Study ◽  
Kleene Algebra

AbstractConcurrent Kleene Algebra (CKA) extends basic Kleene algebra with a parallel composition operator, which enables reasoning about concurrent programs. However, CKA fundamentally misses tests, which are needed to model standard programming constructs such as conditionals and $$\mathsf {while}$$ while -loops. It turns out that integrating tests in CKA is subtle, due to their interaction with parallelism. In this paper we provide a solution in the form of Concurrent Kleene Algebra with Observations (CKAO). Our main contribution is a completeness theorem for CKAO. Our result resorts on a more general study of CKA “with hypotheses”, of which CKAO turns out to be an instance: this analysis is of independent interest, as it can be applied to extensions of CKA other than CKAO.

scholarly journals Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)

2020 ◽  
pp. 378-382
Author(s):  
Hernán Ponce-de-León ◽  
Florian Furbach ◽  
Keijo Heljanko ◽  
Roland Meyer
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Memory Models ◽  
Memory Model ◽  
Complete Analysis ◽  
Concurrent Programs ◽  
Sequential Consistency ◽  
Model Checker ◽  
Safety Properties ◽  
C Programs

Abstract Dartagnanis a bounded model checker for concurrent programs under weak memory models. What makes it different from other tools is that the memory model is not hard-coded inside Dartagnanbut taken as part of the input. For SV-COMP’20, we take as input sequential consistency (i.e. the standard interleaving memory model) extended by support for atomic blocks. Our point is to demonstrate that a universal tool can be competitive and perform well in SV-COMP. Being a bounded model checker, Dartagnan’s focus is on disproving safety properties by finding counterexample executions. For programs with bounded loops, Dartagnanperforms an iterative unwinding that results in a complete analysis. The SV-COMP’20 version of Dartagnanworks on Boogiecode. The C programs of the competition are translated internally to Boogieusing SMACK.

scholarly journals POMDP Models for Assistive Technology

2012 ◽  
pp. 294-314 ◽  
Author(s):  
Jesse Hoey ◽  
Pascal Poupart ◽  
Craig Boutilier ◽  
Alex Mihailidis
Keyword(s):  
Decision Process ◽  
Health And Safety ◽  
Safety Monitoring ◽  
The Elderly ◽  
Assistive Technologies ◽  
Theoretic Model ◽  
Partially Labeled Data ◽  
Ongoing Work ◽  
Markov Decision ◽  
Partially Observable

This chapter presents a general decision theoretic model of interactions between users and cognitive assistive technologies for various tasks of importance to the elderly population. The model is a partially observable Markov decision process (POMDP) whose goal is to work in conjunction with a user towards the completion of a given activity or task. This requires the model to monitor and assist the user, to maintain indicators of overall user health, and to adapt to changes. The key strengths of the POMDP model are that it is able to deal with uncertainty, it is easy to specify, it can be applied to different tasks with little modification, and it is able to learn and adapt to changing tasks and situations. This chapter describes the model, gives a general learning method which enables the model to be learned from partially labeled data, and shows how the model can be applied within our research program on technologies for wellness. In particular, we show how the model is used in four tasks: assisted handwashing, stroke rehabilitation, health and safety monitoring, and wheelchair mobility. The first two have been fully implemented and tested, and results are summarized. The second two are meant to demonstrate how the POMDP can be applied across a wide variety of domains, but do not have specific implementations or results. The chapter gives an overview of ongoing work into each of these areas, and discusses future directions.

scholarly journals Women of Newfangle: Co-Education, Racial Discourse and Women’s Rights in Victorian Ontario

2007 ◽  
pp. 111-134
Author(s):  
Sara Burke
Keyword(s):  
Higher Education ◽  
Social Change ◽  
Middle Class ◽  
Women's Movement ◽  
Vital Role ◽  
Anglo Saxon ◽  
Separate Spheres ◽  
Ongoing Work ◽  
The Right ◽  
Racial Progress

This article argues that during the 1870s, members of the Anglo-Canadian women’s movement targeted university co-education in their first radical assault on separate spheres ideology, deliberately exploiting the discourses of both individual and racial progress to openly contest established definitions of middle-class womanliness. Rather than accept the evolutionist theory that white women’s contribution to the race was solely reproductive – that they were passive recipients of the benefits of male progress – reformers in Ontario argued that Anglo-Saxon women had an active, vital role to play in the ongoing work of racial advancement. Reformers linked the right of middleclass women to higher education to the much larger issue of the continued progress of the Anglo- Saxon race. By championing co-education, members of the women’s movement were promoting a blueprint for social change in which the daughters as well as the sons of the new Dominion would assume their responsibility to regenerate Anglo-Saxon civilization.

The Complex Structure of Health Rights

2020 ◽  
Vol 13 (1) ◽  
pp. 99-110
Author(s):  
Michael Da Silva
Keyword(s):  
Health Care ◽  
Complex Structure ◽  
Philosophical Perspective ◽  
Economic Rights ◽  
Right To Health Care ◽  
Traditional Structure ◽  
Ongoing Work ◽  
The Right ◽  
Health Rights ◽  
Health Justice

Abstract Research on how to understand legally recognized socio-economic rights produced many insights into the nature of rights. Legally recognized rights to health and, by extension, health care could contribute to health justice. Yet a tension remains between widespread international and transnational constitutional recognition of rights to health and health care and compelling normative conditions for rights recognition from both philosophers seeking to identify the scope and structure of the rights and policy scholars seeking to understand how to practically realize such rights (and measure realization of same). This work identifies an overlooked source of these difficulties: the right to health care and other health rights are necessarily ‘complex’, consisting of multiple related, but irreducible, morally valuable components. ‘Complex rights’ do not fit the traditional structure of human rights, so legal recognition of same can appear confused from a philosophical perspective, but there is ample reason to admit complex rights into our moral ontology and doing so can help bridge the divide between global health practices and ongoing work in the philosophy of rights and public policy. Recognition of complex rights admittedly shifts the burden for justifying health rights, but it does so in a way that is instructive for general philosophical analysis of socio-economic rights.

scholarly journals POMDP Models for Assistive Technology

2013 ◽  
pp. 120-140
Author(s):  
Jesse Hoey ◽  
Pascal Poupart ◽  
Craig Boutilier ◽  
Alex Mihailidis
Keyword(s):  
Decision Process ◽  
Health And Safety ◽  
Safety Monitoring ◽  
The Elderly ◽  
Assistive Technologies ◽  
Theoretic Model ◽  
Partially Labeled Data ◽  
Ongoing Work ◽  
Markov Decision ◽  
Partially Observable

This chapter presents a general decision theoretic model of interactions between users and cognitive assistive technologies for various tasks of importance to the elderly population. The model is a partially observable Markov decision process (POMDP) whose goal is to work in conjunction with a user towards the completion of a given activity or task. This requires the model to monitor and assist the user, to maintain indicators of overall user health, and to adapt to changes. The key strengths of the POMDP model are that it is able to deal with uncertainty, it is easy to specify, it can be applied to different tasks with little modification, and it is able to learn and adapt to changing tasks and situations. This chapter describes the model, gives a general learning method which enables the model to be learned from partially labeled data, and shows how the model can be applied within our research program on technologies for wellness. In particular, we show how the model is used in four tasks: assisted handwashing, stroke rehabilitation, health and safety monitoring, and wheelchair mobility. The first two have been fully implemented and tested, and results are summarized. The second two are meant to demonstrate how the POMDP can be applied across a wide variety of domains, but do not have specific implementations or results. The chapter gives an overview of ongoing work into each of these areas, and discusses future directions.

Sign in / Sign up

Export Citation Format

Share Document