Jean-Paul Thibaud

A sonic paradigm of urban ambiances?

This paper intends to investigate urban ambiances through focusing on the world of sounds. Although the aesthetics of everyday life implies employing the whole human sensorium, making it difficult to artificially separate the information received from the individual senses from each other, I explore what can be learned about an ambiance when we just listen to it. In other words, how and under which conditions is it possible to develop a sonic paradigm of urban ambiances? The basic argument is to consider sound as a particularly efficient medium to investigate and develop an account of urban ambiances. Various ideas will be explored in order to answer this question, involving theoretical, epistemological and methodological arguments. Three main directions are accentuated: the first one relates to the tuning into an ambiance, the second relates to the unfolding of an ambiance, and the third relates to the situating within an ambiance.

Urban spaces provide numerous ambiances to be felt with all the senses.

Whether we think of a lively outdoor marketplace or an ordinary parking lot, an attractive historical center or an accessible subway station, the very way we relate to these places is based on the sensory experience they provide. It is a matter of light and colour, sound, smell, touch and heat, as well as the manner in which we walk and talk, move and look, relate and behave. In other words, urban ambiances always create a subtle interweaving of synaesthesia and kinaesthesia, a complex mixture of percepts and affects, a close relationship between sensations and expressions.

To put it succinctly, an ambiance can be defined as a space-time qualified from a sensory point of view. It relates to the sensing and feeling of a place.

Each ambiance involves a specific mood expressed in the material presence of things and embodied in the way of being city dwellers. Thus, ambiance is both subjective and objective: it involves the lived experience of people as well as the built environment of the place 1 . I would like to investigate urban ambiances by focusing on the world of sounds. Although the aesthetics of everyday life implies the whole human sensorium and makes it difficult to artificially separate the information received from the individual senses from each other, I will explore what can be learned about an ambiance when we decide to just listen to it. The basic argument is to consider sound as a particularly efficient medium to investigate and develop an account of urban ambiances. In other words, how and under which conditions is it possible to develop a sonic paradigm of urban ambiances? By asking such a question, I will focus on the relationship between sound and ambiance, and consider the very nature of sonic experience.

Ambiance and Music

To start with, it can be useful to remember that certain forms of music are very closely related to ambiances. Consider Eric Satie's Musique d'ameublement (furniture music) that was composed in order to create a background atmosphere for specific activities such as dinner. We can also think of Brian Eno's Ambient music that aims to create diverse moods appropriate to various times and situations. The set of pieces entitled Music for Airports may be some of the most famous. Of course, from a different perspective, there is also the musical atmosphere produced by Muzak and other companies that offer background music for commercial purposes [START_REF] Sterne | Sounds Like the Mall of America: Programmed Music and the Architectonics of Commercial Space[END_REF].

Those few examples show that the link between music and ambiance has already been explored. Such cases are worth mentioning because they emphasize three important features of an ambiance. With sound -as with ambiance -we are immersed in a milieu. No need to mention the famous surroundability and omnidirectionality of sound. We are surrounded by sounds that propagate all around and come from everywhere at once. In other words, sound places me in the midst of a world (Ong 1981).

1 For an overview of the notion of ambiance, see (Amphoux, Thibaud and Chelkoff 2004) ; (Augoyard 2011) ; [START_REF] Thibaud | The Sensory Fabric of Urban Ambiances[END_REF].

With Muzak, loud speakers are disseminated everywhere in space in order to create a ubiquitous sonic environment. As Sumrell and Varnelis (2005: 118) observed, "if the music is audible, its source is no longer discernable".

Secondly, this kind of music is not designed to be listened to very attentively; it should barely be heard. It operates as a continuous background to everyday life. This is what Michel [START_REF] Chion | Le promeneur écoutant. Essais d'Acoulogie[END_REF] designates as musique-milieu, which tends to accompany everyday activities, as opposed to musique-discours, which involves a linear discourse with a specific beginning and an end. Here again -as with ambiance -these experiences can combine both attention and distraction, they can implement various levels of listening attention. In other words, such sensory environments can be experienced without being noticed, heard without being listened to. Third, there is a direct link between this background music -this ambient music -and the situation in which it is played.

Each composition is designed to fit a specific situation, to induce a specific mood [START_REF] Lanza | Elevator Music. A Surreal History of Muzak, Easy-Listening and other Moodsong[END_REF]. Here again, it is intrinsic to ambiances that they cannot be dissociated from their context of appearing. We sometimes define an ambiance as the pervasive quality of a situation [START_REF] Thibaud | De la qualité diffuse aux ambiances situées[END_REF].

The Multisensoriality of an Ambiance

This discussion of background music demonstrates the close affinity between sound and ambiance. However, in what sense is it legitimate to focus exclusively on sound? Each sensory modality contributes to the fabric of an ambiance and provides its specific phenomenal characteristics. For instance, in his attempt to identify the various features that generate a certain atmosphere of a building, the Swiss architect Peter Zumthor (2006) distinguishes the sound of a space that contributes a g r e a t d e a l toward a "feeling at home", the temperature of a space that helps to temper the environment and to search "for the right mood", the light on things that is experienced "almost as a spiritual quality". Also, Juhani [START_REF] Pallasmaa | The Eyes Of The Skin: Architecture And The Senses[END_REF] aims at developing a sensory architecture that puts the entire body in the centre and integrates all the senses.

Obviously, sound cannot pretend to operate as a substitute for light, temperature, touch or odors in the creating of an atmosphere. If one sense is in no way replaceable by another, why do I focus my investigation on sound exclusively?

Additionally, it has been argued that it is not sound which bears the closest relationship to an atmosphere. In a very interesting and convincing piece of work, Hubertus Tellenbach elaborates a phenomenology of the "oral sense" (smelling and tasting) and demonstrates its strong affinity with atmosphere: "That which precisely characterizes the essence of the sensorial system is that in the feeling of being affected -more than in the affections of the other senses -a homogenization of the state of being human is realized, that is to say: a tuning into an ambiance." (Tellenbach 1983: 17, my translation). In emphasizing the archaïc, immersive and pre-judgemental aspect of the oral sense, Tellenbach achieves an elaboration of the notion of "atmospherics". Based on existential psychology and clinical observations, this research brings back into favour the so-called "lower" senses, showing their importance in the development of human being and the understanding of various pathologies and psychosis. If the oral sense plays such a crucial role in the experiencing of atmosphere, why insist on exploring another sense such as the auditory one? From these few remarks, it seems that the idea of a sonic paradigm of urban ambiances is far from being obvious and cannot be taken for granted. In order to go further, we have to ask ourselves what can be considered specific to the world of sound. The problem is not to reduce an ambiance to its sonic component, or to affirm that only sound can give us an account of what an ambiance is all about. Rather, the idea is to ponder what an ambiance is in terms of sound. What can we learn when we consider an ambiance from a sonic perspective? In a way, it is a heuristics of sound that I am attempting to develop here. This is of course a very ambitious project, and I do not pretend to accomplish it completely. I will simply give three different directions that seem worth exploring in the future. The first one relates to "the tuning into a n ambiance", the second one relates to "the unfolding of an ambiance", and the third one relates to "the situating within an ambiance".

The Tuning into an Ambiance

When we try to describe an ambiance or even to define the very notion of ambiance, we tend to use various terms derived from the science of acoustics or music, terms that are rooted in the verbal history of auditory experience. For instance, an ambiance can be specified by its "tone" (an affective tonality), it involves our ability to be "in tune" with the place, it has something to do with "sympathy" and "harmony"… We speak sometimes of "a vibrant atmosphere"… While our everyday language is predominantly based on visual images, such is not the case with ambiance. The three main properties of vision identified by the philosopher Hans Jonas (1966) -simultaneity, neutralisation and distance -are not accurate to express the very nature of an ambiance. On the contrary, audition appears to be closely related to it. Eugene Minkowski explains it very accurately:

We usually talk, for the phenomena related to sympathy, of harmony, of resonance, of the ability to vibe in unison with or to tune oneself to an ambiance. But why do we use, in this domain, only metaphors coming from the world of sounds? For me, this preference for acoustic 'metaphors', far from surprising, seems completely natural, as it exists for the language which in turn creates it. Those metaphors reveal the structural identity between phenomena of lived synchronism and the world of sounds; the latter, as the former, are based on a fundamental property of life : resonance. [START_REF] Minkowski | Vers une cosmologie[END_REF]: 106, my translation).

For sound -as for ambiance -resonance is not a simple property among others; it is a basic and grounding phenomenon of the entire sensory experience. To sum it up: t h e r e i s no sensation without vibration and resonance, whether it be sound, light or texture (Deleuze 2003). As Elisabeth Grosz comments, relying on Deleuze's philosophy: "sensation, after all is nothing but a vibratory difference capable of resonating bodily organs and the nervous system" (Grosz 2008: 62). To be sure, it is a notion which comes from the world of sound -i.e. resonance -that enables us to elaborate on the unity of the senses and point out their common denominator.

But for now, let's stick with sound and start with an example. Organ builders know perfectly the power of vibrations when they make sure that the low pitch notes of the organ will not cause too many sympathetic vibrations in the stained glasses of the cathedral, in order to prevent breaking them. This is to say that buildings or places are not completely inert or passive, since they respond to and amplify certain resonance frequencies. Thus, it is necessary to adjust the intensity of sounds of the organ to the place. Like the cathedral mentioned above, the body itself operates as a resonance chamber that vibrates to the stimulation of its immediate surroundings. In other words, resonance involves the ability of the body to incorporate and be affected by vibratory forces: its capacity to engage with, be penetrated by and participate in the actual ambiance. As Jean-Luc Nancy very accurately analyzes, "Resonance is at once that of a body that is sonorous for itself and resonance of sonority in a listening body that, itself, resounds as it listens." (Nancy 2007: 40) What I am trying to describe here is not perception but rather sensation; not the way we interpret, recognize and understand the world we perceive, but rather the way we feel and relate to the world we sense. Sensing rather than perceiving. The "pathic" dimension rather than the "gnostic" one:

"by the pathic moment, we mean the immediate communication we have with things on the basis of their changing mode of sensory givenness. Thus, we do not relate the pathic dimension to the fixed or changing properties of the objects, and this means not to objects capable of attracting, frightening, or oppressing us by their properties. The gnostic moment merely develops the what of the given in its object character, the pathic the how of its being as given." (Straus 1963: 12) By pathic, Straus means a mode of immediate communication with the world.

Contrary to the gnostic component that involves apperception and is directed towards the objective features of the surroundings, the pathic sphere is on the side of affectivity and bodily sensation, it is not a mode of knowing. For example, when we enter a new place, we immediately feel its atmosphere and make sense of it. Our body responds to the place in some way or another. We tend to adopt its rhythm and its tonality. We are moved by the gentleness of the whispers, the brightness of the light, the coldness of the winter air or the spiciness of the smell. The ambiance takes hold of us before we are able to clearly identify and represent the actual situation. In other words, ambiance relies strongly on the pathic dimension of sensory experience. Obviously, in everyday life the gnostic and the pathic are closely intertwined, as well as the impressions coming from the various senses. However, Straus demonstrates quite convincingly that acoustic space is particularly relevant regarding pathic experience [START_REF] Boissière | Vers une psychologie du mouvement : l'espace acoustique d'Erwin Straus, entre musique et danse[END_REF]. Because sound occupies and integrates space, reaches and seizes us, it renders orientation and objectivation difficult. To be sure, a tone is not « here » nor « there », it is everywhere. When we look for the source of a sound, when we try to localize it, we still rely on vision and we lose the very nature of acoustic space. Contrary to color that remains attached to the object, sound has the ability to separate itself from its source and liberate itself from directional movement. Such a consideration brings Straus to associate acoustic space with the space of the dance. In both cases, the body tends to move without direction and resonates with its immediate surroundings. Like dance, sound has the ability to embody the pathic dimension of an ambiance.

With sounds -as with ambiances -we do not experience the world from the outside, in front of us, but through it, in accordance with it, as part of it. The sensing subject is nothing but a resonant body that gets in tune and in sync with his environment. Japanese culture and philosophy seem particularly adept in fomenting and developing perspective [START_REF] Nagatomo | Attunement Through the Body[END_REF]). In a way, I become part of what I sense; I tend to merge with the ambiance; my level of tension adjusts to the one of the world. My voice -my way of speaking -tends to sound akin to what I hear. Here, no need for mediation, since the sensing subject and the sensed world are two faces of the same coin. To put it differently, the limit between my body and the world is porous. With sound, the categories of energy, force and tones tend to replace the one of image, representation and forms [START_REF] Zuckerkandl | Sound and Symbol. Music and the External World[END_REF]). To phrase it concisely: with the idea of "resonance", the world of sound makes explicit the very power of attunement to an ambiance. It helps to describe the very process by which I feel and sense the world. This may be why sounds -ambiances are so close to affective and emotional experience. As Yi-Fu Tuan notices: "More important, sound dramatizes spatial experience. Soundless space feels calm and lifeless despite the visible flow of activity in it, as in watching events through binoculars or on the television screen with the sound turned off, or being in a city muffled in a fresh blanket of snow." (Tuan 2003: 16) Do we not say that an ambiance can have good vibes?

The Unfolding of an Ambiance

The second power of sound to be mentioned relates to the unfolding of an ambiance. Sound can help us to record, document and describe the dynamics of an ambiance. Registration of sound can be used to design and develop a sensory ethnography of the urban world. Here, three main arguments should be briefly mentioned.

Firstly, sound cannot be experienced without time. When we define sound as "qualified time", we emphasize time is not a parameter among others, an additional property of sound. Rather, time is the very nature of sound; it is constitutive of sound. As Don Ihde summarizes: "sound embodies the sense of time" (Ihde 2007: 85). This is a very well-known argument, and I am not going to develop upon it too much. When we record or listen to a place, we inevitably sense time passing by, a time that is not an abstract time, a time of clocks, but a qualified time: the slow ending of the day when sounds progressively diminish, the frenzy and excitement of rush hour, when the crowds invade the streets, the quiet pause of a Sunday afternoon when nobody is outside… Thus, if we want to study how an ambiance evolves and develops, we listen to it carefully in order to be able to recompose its internal dynamics. In his project of rhythmanalysis, Henri Lefebvre (1984) pointed out the crucial role of sound for the rhythmanalyst, the one who studies the rhythms and atmospheres of a place.

However, what is interesting about the auditory world is not only its temporal dimension but also its active and generative one. This brings me to the second point. When we listen to an ambiance, we hear an ambiance being made, we hear the process of formation and transformation itself. Indeed, an ambiance is not only to be felt but also to be produced. When we try to understand the way an atmosphere is generated, we have to consider the interaction between the built environment and the social practices it enables and relies on. In other words, an ambiance cannot be reduced to mere sensory qualities resulting uniquely from the architecture or spatial design of a place. We also have to take into account the everyday activities of city dwellers: people walking on the streets, talking to each other, driving their cars, building a new house, mowing their lawns, etc. All those activities are audible and are components of an ambiance.

Sound is not the property of a thing but the result of an action. This can apply for social practices and everyday activities; it can also apply to natural events like when the wind blows or the rain pours and render audible some features of the environment that were silent until then. In any case, sound gives access to what is happening. This is to say that sound is very closely intertwined with movement, gesture and action. Regarding ambiance, it is not only the social activity itself that can be heard but the manner and the conditions in which an action is accomplished. In other words, sound is a very useful medium that can help us document the social expression of an ambiance.

Let me just briefly mention an anecdote related to research carried out years ago, dealing with the ambiances of underground public places.

Together with a colleague of mine -Grégoire Chelkoff -I studied two specific underground public spaces in Paris: the Louvre and the Halles [START_REF] Chelkoff | A m b i a n c e s s o u s l a v i l l e . u n e a p p r o c h e écologique des espaces publics souterrains[END_REF]. We observed that in the Louvre, the very smooth floor enabled, perhaps encouraged, visitors to perform a kind of "sliding step", a way of walking with motions similar to skating. What is interesting is that we noticed this not from visual observation, b u t t h r o u g h the act of listening. In the recordings we made, there was a kind of prolonged smooth sound that we could not immediately identify. After some listening we understood that it was the sound people were making when they were walking. What we were hearing was not simply people walking but the way people were walking, in accordance with the texture of the floor and the characteristics of the place. From this example, we understand that people's practices are constitutive of the production and expression of an ambiance.

Finally, the third point is related to the unfolding of an ambiance. Following the temporal and the generative, we might also highlight the collective dimension. When we listen to an ambiance, we hear the unfolding of social life itself. Ambiances cannot be reduced to a subjective domain, but are rather a public expression of a specific form of life, of a particular way of living together:

The question of sound atmospheres is directly related to the dimension of lifestyles, understood as generators of urban atmospheres. In terms of street noise, it makes a difference as to whether it is customary for people to honk their horns or not, what brand of car they drive, whether radio music can be heard through their open windows, whether the names of goods are shouted out, or 'alluring' music comes from their boutiques. These are just some aspects : through their lifestyles, the inhabitants of the city are also, always, producers of its atmosphere. (Böhme 1998: 11). you hear a place, you hear a specific social organization of sound as well as the way in which people interact and relate to each other. Sound is both the expression and the medium of various modes of social existence; it is closely intertwined with the hurly-burly of social life, with the "multiple as such" [START_REF] Serres | Genesis. Michigan: The University of Michigan Press[END_REF].

In addition, sound can mark the urban character of an ambiance. At a very basic level, the nature of the acoustic signals is quite significant: ongoing traffic noise, compact voices in a crowd, electronic device beeps or background music in public spaces operate as indexes of an urban ambiance. But more fundamentally, the density of micro-events, the loss of intervals and pauses, the reverberated sound of enclosed space and the fast pace of street life plunge us into the urban world. No need to say that sound is a very powerful medium to express the sensory ecology of urban spaces (LaBelle 2010).

Instead of developing this idea, allow me to illustrate this point with two short sound recordings. Both of them relate to the use of loud-speakers for commercial purposes. The first one -Cashier New York -was recorded in New York City, at the checkout counter of a supermarket. The second one -Street vendors Bahia -was recorded in Salvador da Bahia, where several street vendors work close to one another on the same street. We can hear two very different cases of a commercial situation, with their specific temporal, practical and collective features.

To recapitulate, emphasizing the temporal, active and collective dimensions of sound enables us to study and to document the unfolding of an ambiance. It brings us also to a socio-aesthetics of commitment that does not rely only on mere contemplation and reception but also on active involvement in urban life.

Situating within an Ambiance

The last point -the situating within an ambiance -will be just mentioned and not thoroughly developed. Here, it is important to understand that when I speak of ambiance, I am referring to architectural and urban ambiances. The idea is not to explore ambiance or atmosphere in general, as a generic notion, as a wide and vague term. On the contrary, the notion refers to various specific sensory experiences always situated and spatially contextualized. Because sound is context-sensitive, it can help us to clarify the situatedness of each singular ambiance. In other words, the sense of audition is sufficiently accurate to properly qualify and precisely distinguish one ambiance from another. Listen to the recordings, mentioned above, of New York City and Salvador da Bahia and you will very easily hear the difference of atmosphere. Although it may also be possible with smell or temperature, this sensory information cannot be recorded, played back and registered in order to be analyzed carefully afterwards.

However, there is a second reason why sound is particularly adequate to describe architectural and urban ambiances. An ambiance is a complex pervasive quality which brings together and unifies numerous components of a situation. Any ambiance involves at once the characteristics of the built environment; the way people live, behave and interact but also the impact of the weather and the growing presence of technology. Those components are diverse and heterogeneous. If each sense relates to all those variables to a certain extent, I contend that sound is perhaps the most likely to incorporate, assimilate and weave them all together. When you listen to a place you can hear the rain pouring down the pavement, the wind blowing through the trees or the subdued sound of a snowy place; you can hear the reverberation of a small indoor plaza or background traffic noise that disperses through a large open field park; you can hear the fast pace of people passing by or a friendly conversation going on in the crowd; you can hear the ringing of cell phones or the filtered music coming from an Ipod. All those voices intertwine and mix together in a single affective tonality that specifies an ambiance. Victor Zuckerkandl (1973: 105) named this phenomenon "tonal coalescence" when "several tones sounding in conjunction produce one sound sensation".

In a way, the world of sound is sufficiently context-sensitive to unify the variables, conditions and circumstances that generate an ambiance. It enables us to develop transverse tools and interdisciplinary methods that articulate the sensory within the spatial, the social, and the physical. Such is the case of the paradigm of sonic effect -halfway between the sound object of Pierre Schaeffer and the soundscape of Murray Schafer -that "gathers together into unified and harmonious listening what other disciplinary knowledge divides" (Augoyard & Torgue 2006: 11). In other words, while vision tends to implement too great a distance between the perceiver and the perceived, and while olfaction tends to produce overly diffuse and volatile phenomena, audition can mix the affective with the cognitive, the universal with the singular in a very balanced way.

Conclusion

Questioning the possibility of a sonic paradigm of urban ambiances led us to explore the complex relation between sound and ambiance. Sound has proved be a very useful medium to describe the tuning into, the unfolding of, and the situating within an ambiance. Those three perspectives helped me to approach the puzzling notion of ambiance by revealing some of its main features: the emphasis on sensing over perceiving; the crucial role of resonance and affective tonality; the importance of internal dynamics, everyday gestures and social forms of life; the embeddedness in sensory urban ecology; the phenomenon of coalescence that unifies the diverse; the articulation between the spatial, the social and the physical. I briefly mentioned how an ambiance involves the very nature of lived experience, the dynamics of sensory environment and the complexity of urban situations.

If sound and ambiance are so closely related, it is because they both question the idea of a clear distinction between the perceiver and the perceived, the subject and the object, the inside and the outside, the individual and the world. Instead of relying on a dualistic and substantialistic mode of thinking, they require an alternative to an ontology of the thing that considers the medium, the fluxes and the "quasi-objects" (Serres 1982). and ambiance enable us to emphasize the "in-between" and the "in-the-middle", and through them a relational thought can develop. From this final argument, we can try to


Olivier Gasquet
email: olivier.gasquet@irit.fr

Valentin Goranko

Francois Schwarzentruber

Big Brother Logic: Logical modeling and reasoning about agents equipped with surveillance cameras in the plane †

Keywords: I.2.4 [Artificial Intelligence]: Knowledge Representation Formalisms and Methods-Modal logic; I.2.11 [Artificial Intelligence]: Distributed Artificial Intelligence-Intelligent agents, Multiagent systems Theory, Algorithms, Verification logical reasoning, multi-agent systems, surveillance cameras, vision, knowledge, model checking, satisfiability testing

We consider multi-agent scenarios where each agent controls a surveillance camera positioned in the plane, with fixed position and angle of view, but rotating freely. The agents can thus observe the surroundings and each other. They can also reason about each other's observation abilities and knowledge derived from these observations. We introduce suitable logical languages for reasoning about such scenarios which involve atomic formulae stating what agents can see, multi-agent epistemic operators for individual, distributed and common knowledge, as well as dynamic operators reflecting the ability of cameras to turn around in order to reach positions satisfying formulae in the language.

We introduce semantics of our basic logic BBL and its extensions on natural geometric models, as well as formal Kripke semantics for them in vision-based finite abstractions of the geometric models. We discuss the expressiveness of our logical languages and provide their translations in PDL style. Using these translations we develop algorithms and obtain complexity results for model checking and satisfiability testing for BBL and its extensions. Notably, we show that even for the extension with common knowledge, model checking remains in PSPACE. Finally, we discuss some further extensions: by adding obstacles, positioning the cameras in 3D or enabling them to change positions.

INTRODUCTION

Modeling and study of multi-agent systems that involve intelligent agents combining perceptual and reasoning abilities is a major field of research and applications of AI. An important issue in that field is the analytic processing of visual perception and visual communication, where the main problem is how to represent and reason logically about the visual information that the intelligent agents receive from the environment and from each other. This creates not only agents' knowledge about the surrounding world, but also about each other's knowledge about that world, etc. and that knowledge affects and guides their intelligent behavior.

In this paper we address these issues by considering multiagent scenarios where each agent controls a stationary surveillance camera positioned in the plane. In the basic framework presented here each camera has a fixed position and angle of view, but can rotate freely around its axis. Through the cameras, the agents can observe the surrounding world and each other. We adopt some basic assumptions about these scenarios, in order to simplify or idealize them: ✄ We identify, conceptually and physically, the agents with their cameras. Thus, we can talk about agents seeing objects and about cameras' knowledge.

✄ We assume that the cameras/agents are positioned at single points in the plane, and are transparent. These assumptions can be easily relaxed and non-transparent cameras/agents of real sizes can be considered, without major modifications of the framework and the obtained results, by simply treating them both as cameras and as obstacles.

✄ We assume that the only objects of interest for any agent in our scenarios are the other cameras/agents. This assumption is not practically restrictive, because one can assume that all other objects of interest are agents equipped with cameras, too, which cannot see anything or we are simply not interested in what they can see and know.

✄ Here we also assume that the agents and their cameras are stationary. In reality these are often mobile. Adding mobility of cameras leads to models where only the set of agents and the vision angles of their cameras are specified, but not their positions. We leave the model checking and satisfiability problems for the case of mobile cameras to a follow-up work.

✄ In the stationary setup we assume that every agent knows the exact positions (but not the directions of vision) of all agents/cameras, even of those that the agent does not see currently. This assumption is certainly well justified if agents are endowed with some memory, as they can turn around to observe and memorize the positions of the others.

We introduce suitable logical languages for reasoning about such scenarios which involve atomic formulae stating what agents can see, multi-agent epistemic operators for individual, distributed and common knowledge, as well as dynamic operators reflecting the ability of cameras to turn around in order to reach positions satisfying formulae in the language.

Here we are interested not only in what agents can see, but also in the knowledge they can derive from their visual perception. The agents' knowledge that we model and study in our framework is about other agents' observation abilities and about their direct and iterated knowledge derived from such observations. A subtle issue arises here, of how vision and knowledge are related. At first glance, it seems that agents only know about other agents' knowledge what they can immediately derive from what they can see regarding the observational abilities of those other agents. We show that this is not quite so, as there is a non-trivial deductive aspect in the analytic knowledge that agents can acquire.

We introduce semantics for our logical languages on natural geometric models, as well as formal Kripke semantics for them in vision-based finite abstractions of the geometric models. We then discuss their expressiveness and provide translations for them in the style of Propositional Dynamic Logic PDL [START_REF] Harel | Dynamic Logic[END_REF]. Using these translations we develop algorithms and obtain complexity results for model checking and satisfiability testing for the basic logic BBL that we introduce here and for some of its extensions. The key observations that enables our model checking and satisfiability testing procedures is that, while the set of geometric models over a configuration of cameras with fixed positions is infinite, the set of their vision-based abstractions, obtained by identifying models where each agent can see the same configuration of agents, is finite.

Finally, we discuss some important extensions of the present work: adding obstacles, positioning the cameras in 3D or enabling them to change positions. Our work has potential applications to automated reasoning, formal specification and verification of observational abilities and knowledge of multirobot systems.

We are aware of very few related previous studies on the topic, but not involving logical reasoning, e.g., [START_REF] García | Agent-based coordination of cameras[END_REF], [START_REF] Bustamante | Multi-camera and multi-modal sensor fusion, an architecture overview[END_REF]. They have mainly considered technical, architectural and knowledge representational aspects of agent-based systems of multicamera surveillance and information processing. To our knowledge, the only previous study related to logical reasoning in such scenarios is the one represented by [START_REF] Schwarzentruber | Seeing, knowledge and common knowledge[END_REF] and [START_REF] Balbiani | Agents that look at one another[END_REF], which is the main precursor of the present work.

The paper is organized as follows: after brief preliminaries in Section 2, we introduce the logics BBL and some extensions in Section 3, discuss their expressiveness and provide translations to PDL in Section 4 and develop algorithms and obtain complexity results for model checking and satisfiability testing in Section 5. We then introduce and discuss briefly some further extensions in Section 6 and end with the concluding Section 7.

PRELIMINARIES

Multi-agent epistemic models and logics

For the necessary background on modal logic refer e.g., to [START_REF] Blackburn | Modal Logic[END_REF]. Here we only give the basics on multi-agent epistemic models and logics. For the conceptual aspects or further technical background refer to e.g., [START_REF] Fagin | Reasoning about Knowledge[END_REF] or [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF].

A multi-agent epistemic structure for a set of agents Agt is a tuple S = Agt, St, {∼a| a ∈ Agt} , where St is the set of states (possible worlds) and ∼a is the epistemic indistinguishability relation on St of the agent a. In our setup there will be no abstract atomic propositions, only concretely interpreted ones, so epistemic structures and models will coincide.

We consider fully expressive multi-agent epistemic logics, extending classical (propositional) logic by adding epistemic operators for individual knowledge Ka, for each agent a, and for group knowledge K A , distributed knowledge D A , and common knowledge C A for every non-empty group of agents A.

Thus, the formulae of the language of the multi-agent epistemic logic MAEL are defined as follows:

ϕ := p | ¬ϕ | ϕ ∧ ϕ | Kaϕ | K A ϕ | D A ϕ | C A ϕ
, where p ranges over a fixed set of atomic propositions PROP, a ∈ Agt and A is a non-empty subset of Agt.

The formal semantics of the epistemic operators at a state in a multi-agent epistemic model M = (Agt, St, {∼a| a ∈ Agt}, V ) is given by the following truth definitions:

(Ka) M, q |= Kaϕ iff M, q ′ |= ϕ for all q ′ such that q ∼a q ′ . (K A ) M, q |= K A ϕ iff M, q ′ |= ϕ for all q ′ such that q ∼ E A q ′ , where

∼ E A = a∈A ∼a. (C A ) M, q |= C A ϕ iff M, q ′ |= ϕ for all q ′ s.t. q ∼ C A q ′ , where ∼ C A is the transitive closure of ∼ E A . (D A ) M, q |= D A ϕ iff M, q ′ |=
ϕ for all q ′ such that q ∼ D A q ′ , where ∼ D A = a∈A ∼a.

Flatland

Interaction between visual perception and knowledge has been studied in [START_REF] Balbiani | Agents that look at one another[END_REF], in a logical framework based on the following language, where a, b are agents:

(L ✄,K ) φ ::= a✄b | ¬φ | φ ∨ φ | Kaφ
The atomic proposition a✄b reads "agent a sees agent b".

The language L ✄,K has no abstract atomic propositions. The primary intended models are geometric models where each agent is located at a point in the space and sees a half-space. Different agents are located at different points and every agent a who can see another agent b can also see b's direction of vision. An abstract semantics is based on Kripke models where the possible worlds are geometric models. The indistinguishably relation ∼a for agent a in such Kripke model is defined as follows: two worlds w and u are such that w ∼a u iff the agents seen by agent a are the same and are located in the same way in both w and u.

Two variants of this framework have been studied in [START_REF] Balbiani | Agents that look at one another[END_REF]: Lineland, where the space is 1-dimensional, and Flatland, where the space is 2-dimensional, i.e., a plane. Figure 1 shows two possible worlds in Flatland that are indistinguishable for agent a, because they look the same in the parts which a can see. Note that a sees both b and c in both worlds, so a can see that b sees c, and this is the case in every world which is indistinguishable from these for a, hence a knows that b sees c. In fact, as shown in [START_REF] Schwarzentruber | Seeing, knowledge and common knowledge[END_REF], Ka(b✄c) is equivalent to a✄b ∧ a✄c ∧ b✄c. On the other hand, a does not see d and e in any of these worlds, so a does not know whether d sees e in any of them. In fact, d sees e in world w and d does not see e in world u. In that framework, the model checking problem takes as an input the description of a possible world w (positions and directions of agents) and a formula φ in L ✄,K and asks whether φ holds in w. The satisfiability problem takes as an input a formula φ in L ✄,K and asks whether there exists a world w satisfying φ. It has been proved in [START_REF] Balbiani | Agents that look at one another[END_REF] that both model checking and satisfiability testing are PSPACEcomplete for Lineland and are respectively PSPACE-hard and in EXPSPACE for Flatland.

First-order Theory of the Reals

Consider the following first-order language LF for fields:

φ ::= (e > 0) | (e = 0) | ¬φ | (φ ∧ φ) | ∀xφ | ∃xφ
where e is a polynomial expression over variables x, y, . . .. LF has a standard interpretation in the field of reals R. The problem of checking whether a closed formula of LF is true in R is in EXPSPACE (see [START_REF] Tarski | A decision method for elementary algebra and geometry[END_REF] for the historically first decision procedure and [START_REF] Ben-Or | The complexity of elementary algebra and geometry[END_REF] for the description of an algorithm that runs in EXPSPACE) We will only need to solve that problem for the existential fragment of LF , i.e., for sentences of the form ∃x1 . . . ∃xnψ where ψ is open, for which the truthchecking problem in R is PSPACE-complete (see [START_REF] Canny | Some algebraic and geometric computations in PSPACE[END_REF]) and we will use the algorithm described there in subsection 5.3.

LOGICS FOR AGENTS WITH STATION-ARY SURVEILLANCE CAMERAS

Hereafter we fix a set of agents Agt = {a1, . . . , a k }.

Here we introduce our basic logic for stationary cameras, which we dub Big Brother Logic, or BBL for short.

Languages

The basic language of BBL involves the Flatland operator ✄, the individual knowledge epistemic operators {Ka} a∈Agt , plus the turning (diamond) operator a , where a φ, means "a can turn around his position so that φ holds". Notation:

[ a ] := ¬ a ¬. We also introduce the following extensions:

• BBL C : BBL plus all C A for every group of agents A.

• BBL D : BBL plus all D A for every group of agents A.

• Combinations of the above.

Additional operators: a ⊲⊳ b, meaning "a sees b and b sees a" and B (abc), meaning "b is between a and c".

Semantics

We will introduce 3 different but equivalent types of models for the logic BBL.

Geometric models

Camera configurations are formally represented by geometric models defined in the Euclidean plane R 2 (or just a region) as follows. Every agent's camera is associated with a position (a point in the plane), an angle of view and a unit vector representing the direction of its vision. Formally:

Definition 3.1. Let U be the set of unit vectors of R 2 .
A geometric model is a tuple (pos, dir, ang) where:

• pos : Agt → R 2 ; • dir : Agt → U ; • ang : Agt → [0, 2π).
We denote Cp,u,α the sector that begins in point p from direction u turning in positive (counter-clockwise) direction, and has angle width α. We assume that different agents have different positions, every camera can "see" everything inside its sector of vision, including the positions and the directions of vision of all agents positioned there, but can see nothing outside of it. All cameras can turn at any angle.

Kripke structures and models

Now, we introduce Kripke structures in which the possible worlds are geometric models. Definition 3.2. Given pos : Agt → R 2 and ang : Agt → [0, 2π), we define a Kripke structure M = (pos, ang, D, R) where D is the set of possible functions dir : Agt → U and R assigns to each agent a the following equivalence relation:

Ra = {(dir, dir ′ ) ∈ D 2 | for all b = a, dir(b) = dir ′ (b)}
The truth of formulae is evaluated in such Kripke structures with additionally specified direction function dir ∈ D. The truth conditions are defined as follows. We define knowledge as in the logic of Flatland: an agent a knows a property φ iff φ holds in all possible worlds that are compatible with what a sees. Those possible worlds can only differ from the actual world in the positions of the agents not seen by agent a. Formally, the semantics of all epistemic operators is given as in Section 2.1 by regarding the relation ∼a as follows: dir ∼a dir ′ iff the set of agents seen by a in dir and dir ′ are the same and they have the same directions of view. The difference with the approach described in subsection 2.2 is that here agents have common knowledge of the positions of all agents.

Note that if all agents seen by camera a are in the interior of its sector of vision, then a slight change of the direction of vision of a camera may not change what the respective agent sees, so all cameras would see the same objects if they are rotated at sufficiently small angles. This naturally defines an equivalence relation over worlds in pointed Kripke models where equivalent worlds satisfy the same ✄-propositions. Formally, given a Kripke structure M = (pos, ang, D, R) and dir, dir ′ ∈ D, we define:

dir ≡ dir ′ iff (∀a, b ∈ Agt : M, dir |= a✄b iff M, dir ′ |= a✄b).
The equivalence class of dir with respect to ≡ will be denoted by dir. Since Agt is finite, there are finitely many equivalence classes w.r.t. a given Kripke structure (see prop. Proof. Let (dir, dir ′ ) ∈ (≡ •Ra), and let dir ′′ be the same as dir but with dir ′′ (a) = dir ′ (a). Then (dir, dir ′′ ) ∈ Ra and dir ′′ ≡ dir ′ . Similarly the other way round.

All these Kripke structures are infinite. We give below an equivalent definition for the semantics based on their quotients w.r.t the equivalence relation ≡.

Direction-based and vision-based abstractions of Kripke models

Given a Kripke structure M = (pos, ang, D, R) the directionbased abstraction of M is the Kripke model KM = (W , R, s) with valuation s as follows:

• W = {dir | dir ∈ D};
• R maps each agent a to the equivalence relation

Ra = {(dir, dir ′ ) | (dir, dir ′ ) ∈ (≡ •Ra)};
• for all w ∈ W : w ∈ s(a✄b) iff M, w |= a✄b.

Proposition 3.1. Let G = (pos, dir, ang) be a geometric model, M be the Kripke structure extracted from G and KM be the direction-based abstraction of M. Then the mapping h : D → W defined by h(dir) = dir is a bounded morphism from M onto KM, and consequently, a bisimulation.

Proof. We check the bisimulation conditions:

Atomic harmony: M, dir |= a ✄ b iff KM, dir |= a ✄ b for any dir ∈ D, by definition. Forth: If dir, dir ′ ∈ D and (dir, dir ′ ) ∈ Ra then (h(dir), h(dir ′ )) ∈ Ra by definition of Ra. Back: If (h(dir), w) ∈ Ra for some w ∈ W then w = dir ′ for some dir ′ ∈ D such that (dir, dir ′ ) ∈ (≡ •Ra). Then there is dir ′′ ∈ D s.t. dir ≡ dir ′′ , hence h(dir) = h(dir ′′ ) and (dir ′′ , dir ′ ) ∈ Ra. Corollary 3.1. For all formulas φ ∈ BBL, we have that M, dir |= φ iff KM, dir |= φ.
In fact, each dir ∈ W is entirely characterized by the possible families of sets -one for each camera -of other agents that the camera can see in a glance if suitably turned. Because of this, we can identify a possible world with the tuple stating for each agent the set of other agents that it sees. Of course, we can precompute theses tuples, and also for each agent a we can pre-compute the family Sa of the sets of agents that can be seen at the same time by a, by using standard analytic geometry (we omit the routine details). Definition 3.3. Formally (where dir ∈ D):

• Γ dir a = {b ∈ Agt | pos(b) ∈ C pos(a)
,dir(a),ang(a) } is the set a sees in direction given by dir;

• (Γ dir a ) a∈A is the tuple of sets of agents each agent sees in directions given by dir;

• Sa = {Γ dir a | u ∈ U };
is the family of all sets of agents a can see when turning. Proof. Let a be an agent and start turning the camera clockwise. The set of agents seen by a's camera only changes when one of the two boundary rays of the sector of vision of the camera passes through an agent. In one full circle each of these rays passes through k -1 agents.

A direction-based abstract model can be equivalently defined as follows.

Definition 3.4. A vision-based abstract model is a triple N = (V, T, σ) where:

• V = {(Γ dir a ) a∈Agt | for all a ∈ Agt, dir ∈ D}; • T maps each agent a to the equivalence relation Ta = {((Γ dir a ) a∈Agt , (Γ dir ′ a ) a∈Agt ) | for all b = a, Γ dir b = Γ dir ′ b } • for all (Γ dir a ) a∈Agt ∈ V : (Γ dir a ) a∈Agt ∈ σ(b✄c) iff c ∈ Γ dir b .
The following can be shown by direct verification: We will henceforth drop the superscript dir for possible worlds.

As well σ will be omitted in models since it can be deduced. A BBL formula is satisfiable iff it is true in some geometric model (hence, in some abstract Kripke structure or in a vision-based abstraction); it is valid iff it is true in every geometric model.

EXPRESSIVENESS AND EXTENSIONS

Expressing properties and specifications

The language of BBL and its extensions can express various natural specifications regarding the visual abilities and knowledge of the agents. Here are some examples in BBL and in BBL CD :

• a✄b → Ka[ b ](a✄b): "If a can see b, then a knows that whichever way b turns around, this will remain true."

• (b✄a ∧ b ✄c) ∧ K b a ((a✄b ∧ a✄c) → Kb Ka(b✄a ∧ b ✄c):
"If agent b sees a but not c and knows that a can turn around so as to see both b and c then b consider it possible that a knows that b sees a but not c."

• (a ⊲⊳ b) → C a,b (a ⊲⊳ b): "If a and b see each other, then this is a common knowledge amongst them."

• K a,b ( a (a✄b) ∧ b (b✄a)) → C a,b ( a b (a ⊲⊳ b)).
"If a and b know that each of them can turn around to see the other, then it is a common knowledge amongst them that they can both turn so as to see each other."

• a (a✄c ∧ a✄d) ∧ b (b✄d ∧ b✄e) → a b (D a,b c✄e ∨ D a,b c ✄e)
. "If a can turn around so as to see both c and d and b can turn around so as to see both d and e then both a and b can turn around so as to make it a distributed knowledge amongst them whether c sees e." (The reader is invited to check by hand the validity of this formula.)

Defining betweenness and collinearity

Assuming that the cameras' angles of vision are strictly less that 2π, the relations of betweenness and collinearity can be expressed in the language of BBL as follows:

• The formula [ a ](a✄b → a✄c) is true in a geometric model precisely when c lies on the ray starting at a and passing through b, i.e., when b is between a and c or c is between a and b.

• Therefore, the formula [ a ](a✄b → a✄c) ∧ [ b ](b✄a → b✄c) is true in a geometric model precisely when c lies strictly between a and b. Thus, we can define

B (acb) := [ a ](a✄b → a✄c) ∧ [ b ](b✄a → b✄c)

Relations between vision and knowledge

Clearly, seeing and visual knowledge are closely related: an agent knows that he sees whatever he sees: a✄b → Kaa✄b and knows that he does not see whatever he does not see: a ✄b → Kaa ✄b. On the other hand, there is more in the agent's visual knowledge than what he can see directly. For instance, the following is valid for any agents a, b, c1, c2, e, even if a does not see b:

a✄c1 ∧ a✄c2 ∧ B (c1ec2) → Ka(b✄c1 ∧ b✄c2 → b✄e)
Thus, a has non-trivial (i.e., not logically valid) knowledge about b's visual abilities.

PDL-like form of BBL

Here we will adopt a different, PDL-like perspective on the logic BBL. For background on the propositional dynamic logic PDL refer e.g., to [START_REF] Harel | Dynamic Logic[END_REF]. We can consider every sequence of (non-deterministic) turns of cameras as a program, where turning the camera of an agent a at an unspecified angle is an atomic program, denoted by a . Besides, we can consider tests as atomic programs and build complex programs by applying compositions, unions and iterations to these, like in PDL. The technical advantage is that, as we will show, all knowledge operators can be represented in terms of suitable programs, and eventually the whole language of BBL and all of its extensions considered here can be translated to versions of PDL.

More precisely, let us first introduce a two-sorted language, denoted BBLP DL, with sorts for formulae and for programs, as follows, where a, b ∈ Agt.

φ ::= a✄b | ¬φ | φ ∨ φ | [γ]φ; γ ::= a | φ? | γ; γ | γ ∪ γ
The intuitive meaning of the program operations is as in PDL, e.g., φ? is the program that tests whether φ is true or not, γ1; γ2 is the sequential composition of γ1 and γ2. γ1 ∪ γ2 represents the non-deterministic choice between γ1 and γ2. The formula [γ]φ is read as "after all executions of γ, the property φ holds". We also define the dual operator γ by γ φ := ¬[γ]¬φ, meaning "there exists an execution of γ such that φ holds afterwards". The formal semantics in a vision-based abstraction model N = (V, T ) and a world v ∈ V is defined as follows:

• N, v |= [ a ]φ iff for all u ∈ Ta(v), N, u |= φ; • N, v |= [φ?]ψ iff N, v |= φ → ψ; • N, v |= [γ1; γ2]φ iff N, v |= [γ1][γ2]φ; • N, v |= [γ1 ∪ γ2]φ iff N, v |= [γ1]φ or N, v |= [γ2]φ.
For instance, the program "if a does not see b then a turns" is represented by γ = (¬a✄b)?; a .

Expressing the knowledge operators

Now, we will show how to simulate knowledge operators in terms of programs in BBLP DL.

Expressing the individual knowledge operators

The (individual) knowledge operator Ka can be simulated with the following program, where {b1, . . . , bn} = Agt \ {a}: γ K a = a✄b1? ∪ (a ✄b1?; b1 ) ; . . . ; a✄bn? ∪ (a ✄bn?; bn ) Indeed, each program a✄bi? ∪ (a ✄bi?; bi ) can change the direction of view of bi if and only if a does not see bi, except when bi is a. Thus, the program γ K a may turn arbitrarily all agents, other than a, that are not seen by a, which reflects precisely the semantics of Ka. Group knowledge operator K A is then simulated by the program:

γ K A = a∈A γ K a .

Expressing distributed knowledge

The distributed knowledge operator D A is simulated with the following program, where {b1, . . . , bn} = Agt \ A:

γ D A =
a∈A a✄b1? a∈A a ✄b1? ; b1 ; . . . ;

a∈A a✄bn? a∈A a ✄bn? ; bn

The construction a∈A a✄bi? a∈A a ✄bi? ; bi , as in the translation of individual knowledge operator, is a program that turns agent bi if and only if no agent in A sees it. This reflects precisely the semantics of D A .

Expressing common knowledge

In order to simulate the common knowledge operator C A , we need to add the iteration operator * in the language, that is, if γ is a program then γ * is the program that repeats γ any finite number of times. The resulting language is called BBLP DL * . The semantics is defined on a vision-based abstraction model N = (V, T ) and v ∈ V as follows:

• N, v |= [γ * ]φ iff N, v |= [γ] n ψ for all integers n ≥ 0, where [γ] 0 φ = φ and [γ] n φ = [γ][γ] n-1 φ for n ≥ 1.
Common knowledge among a group A = {a1, . . . , a k } can be simulated by: γ C A = γa 1 ; . . . ; γa k * . As the program γa i represents the epistemic relation for agent ai, the program γ C

A corresponds to taking an arbitrary finite path along the epistemic relations for all agents in A. Note that this simulation is correct because the programs γa i are reflexive and commute with each other.

Translation into BBLP DL and BBLP DL *

Let τ be the translation from BBL into BBLP DL and BBLP DL * defined by: τ

(a✄b) = a✄b, τ (φ1 ∨ φ2) = τ (φ1) ∨ τ (φ2), τ (¬φ) = ¬τ (φ), τ (Xαφ) = γ X α τ (φ) (X is K, D or C).
The next claim follows immediately from the constructions of the knowledge simulating programs.

DECISION PROCEDURES

In this section, we address the model checking problem and the satisfiability problem for BBL and its extensions. For any of these languages L, the model checking problem MC(L), is defined as follows:

Input: a geometric model G = (pos, dir, ang) and a formula φ of L.

Output: 'yes' iff N, v |= φ where N is the vision-based abstraction of G.

The satisfiability problem SAT(L) is defined as follows.

Input: a formula φ in L;

Output: 'yes' iff there exists a geometric model G = (pos, dir, ang) such that N, v |= φ where N is the visionbased abstraction of G.

Upper-bound for MC(BBLPDL * )

The procedure for the model checking problems above consists in two stages: first compute sets Sa (def. 3.3) in the vision based abstraction model (see Definition 3.4) from the geometric model (see Definition 3.1) and then do model checking on worlds of the vision based abstraction model.

Computing the vision-based abstraction model

Let us consider a vision based abstraction model and an agent a. For computing the set Sa, we consider a polar coordinate system centered in pos(a) and we consider all agents b = a as a list sorted by angles. We perform a scan of all agents b = a and we compute the possible sets of agents whose positions are in a sector centered in pos(a) and of angle ang(a). The set of those sets is exactly Sa. This can be achieved in linear time in the size of the vision based abstraction model and the reader can find the pseudo-code in the technical report [START_REF] Gasquet | Big brother logic: Logical modeling and reasoning about agents equipped with surveillance cameras in the plane (long version)[END_REF] . The idea is to identify the positions of the sector of vision of a where one of the boundary rays passes through some of the other agents, and determine the sets of agents seen by a in those positions.

Upper-bound results for model checking

Now, we design a procedure mc for model checking. The specification of mc(Γ, φ) is to return true iff N, Γ |= φ where N = (V, T ) is the vision-based abstraction model and Γ ∈ V . The routine mc is very standard and the only interesting case concerns the model checking of a formula of the form [γ]ψ where γ is a program, given by a regular expression. This case relies on a subroutine path? whose specification is: path?(Γ, Γ ′ , γ) returns true iff there is a γ-path from Γ to Γ ′ , i.e. a path in the graph (V, T ) whose labels match the regular expression γ. For instance, if Γ(Ta

• Ta • RT b)Γ ′ ,
then there is a ( a ;( a ; b ) * )-path from Γ to Γ ′ and therefore path? Γ, Γ ′ , ( a ;( a ; b ) * ) is true.

We want to prove that this model checking procedure works in PSPACE. All cases are straightforward except that of γ = γ * 1 . In order to treat this case, we introduce a new construction of program: γ = γ m 1 where m is an integer written in binary. The procedure path? uses the following simple observation: If there is a γ * 1 -path from Γ to Γ ′ then there is a γ m 1 -path, where 0 ≤ m ≤ 2 k 2 (recall that k = #Agt). Thus, for the case of γ * 1 , we look for the existence of a γ m 1 -path from Γ to Γ ′ for some m ∈ {0, . . . , 2 k 2 }. Now, for the case γ m 1 when m > 1 we use the Divide and Conquer method and browse all possible 'intermediate' worlds Γ ′′ in a γ

⌊ m 2 ⌋ 1 -path from Γ to Γ ′ , that is, there is a γ ⌈ m 2 ⌉ 1
-path from Γ to Γ ′′ and a γ m 1 -path from Γ ′′ to Γ ′ . The resulting model checking procedure runs in polynomial space. The reader can find the pseudo-code of path? and mc in the technical report [START_REF] Gasquet | Big brother logic: Logical modeling and reasoning about agents equipped with surveillance cameras in the plane (long version)[END_REF] .

Proposition 5.1. MC(BBLP DL * ) is in PSPACE.

Lower-bound results for model checking

Unsurprisingly, the lower-bound is reached even without the star operator in the language: Proposition 5.2. MC(BBLP DL) is PSPACE-hard.

Proof. We will give a polynomial reduction of the satisfiability problem SAT-QBF for quantified Boolean formulas (QBF), which is PSPACE-complete [START_REF] Sipser | Introduction to the Theory of Computation[END_REF], to MC(BBLP DL). Consider a QBF ∃p1∀p2 . . . Qnpnψ(p1, . . . , pn) where Q k is ∃ if k is odd and ∀ if k is even and where ψ(p1, . . . , pn) is Boolean formula over the atomic propositions p1, . . . , pn. Let Agt = {a0, a1, . . . , am}. We build an instance (G, φ), where G = (pos, dir, ang), for MC(BBLP DL) as follows:

• pos(ai) = (i, 0); dir(ai) = (-1, 0); ang(ai) = π 4 ;

• φ = a1 [ a2] . . . Oiψ ′ where Oi is ai if i is odd and

[ ai] if i is even and ψ ′ is the formula ψ in which we have replaced all occurrences of pi by ai ✄a0.

Since each of the cameras positioned as above can independently be turned so as to see a0 and it can also be turned so as not to see a0, the formula ∃p1∀p2 . . . Qnpnψ(p1, . . . , pn) is true in the quantified Boolean logic QBL iff N, v |= φ where N is the vision-based abstraction model of G.

Theorem 5.1. Let BBL -be the fragment of BBLP DL without turning operators but with the knowledge operators. Then MC(BBL -) is PSPACE-hard.

Proof. The proof is similar to the proof of Proposition 5.2 (and to the proof for the MC problem in Lineland, in [START_REF] Balbiani | Agents that look at one another[END_REF]). We provide a polynomial reduction of the SAT-QBF problem to MC(BBL -) as follows. Consider a QBF formula ∃p1∀p2 . . . Qnpnψ(p1, . . . , pn) where Q k = ∃ if k is odd and Q k = ∀ if k is even and where ψ(p1, . . . , pn) is Boolean formula over the atomic propositions p1, . . . , pn. We build an instance G = (pos, dir, ang), φ for MC(BBL -) as follows:

• pos(ai) = (2i, 0); pos(bi) = (2i + 1, 0);

• dir(ai) = (-1, 0); dir(bi) = (-1, 0); • ang(ai) = π 4 ; ang(bi) = π 4 ; • φ = Ka 1 (a2 ✄a1 ∧ Ka 2 (a3 ✄a1 → . . . ...ψ ′ ) . . . ) where ψ ′
is the formula ψ in which we have replaced all occurrences of pi by bi ✄a1.

Again, we claim that the formula ∃p1∀p2 . . . Qnpnψ(p1, . . . , pn) is true in quantified Boolean logic iff N, v |= φ where N is the vision-based abstraction model of G. The idea encoded in that formula is that the knowledge operators Ka i and Ka i serve respectively as universal and existential quantifiers over the truth values of the boolean variable pi, while the guards aj✄a1 ensure that the agents' cameras are positioned so as to enable each of these truth values.

Corollary 5.1. The model checking problem for BBL C , BBL D and any combination is PSPACE-complete.

Upper-bound for satisfiability

Now we address the problem of existence of a placement of cameras satisfying a given formula φ of BBLP DL * . Proposition 5.3. SAT(BBLP DL * ) is in PSPACE.

Proof. The satisfiability testing procedure of a formula φ works as follows. First, we guess the set Sa for each agent a. Each Sa contains at most O(k) sets of agents each of them containing at most k = #Agt agents. Thus, it is possible to guess a collection of sets (Sa) a∈Agt , where each Sa is a set of size at most O(k 2 ) in polynomial time. Now, we have to check that there exists a geometric model G from which we can derive the collection (Sa) a∈Agt . That boils down to finding suitable positions and angles of vision for all cameras, consistent with the collection (Sa) a∈Agt . The key point is that we can express the existence of such model in the existential fragment of the first-order theory of the field of reals which is the same as the FO theory of realclosed fields [START_REF] Canny | Some algebraic and geometric computations in PSPACE[END_REF] and can be decided in polynomial space. Once we know the family (Sa) a∈Agt to be consistent, we compute the abstract vision-based model N induced by (Sa) a∈Agt . We then select a set Γa ∈ Sa for each agent a. We finally check whether N, (Γa) a∈Agt |= a1 . . . an φ where Agt = {a1, . . . , an}.

For that purpose we call mc((Γa) a∈Agt , a1 . . . an φ) where the procedure mc is the procedure for the model checking. Oi is ai if i is odd and [ ai ] if i is even and ψ ′ is the formula ψ in which we have replaced all occurrences of pi by ai ✄a0.

Lower-bound for satisfiability

Corollary 5.2. The satisfiability problem for BBL C , BBL D and any combination is PSPACE-complete.

FURTHER EXTENSIONS OF THE BBL

The present work only considers a simplified and idealized scenarios of stationary cameras placed in the plane and without any obstacles to their vision. It is amenable to several natural and important extensions which we only briefly discuss here. The technical details and respective results will be presented in an extended follow-up work.

Adding obstacles

In many real life scenarios the visibility by the cameras of the objects of interest, including other agents, is impaired by stationary or moving obstacles. Here we only sketch how our framework can be extended by adding stationary obstacles. In geometric models, these are represented by their shapes placed in the plane, as in the figure below. In order to take obstacles into account, we have to modify the scan used to compute the sets Sa. For instance, In the example above, when we compute Sa, the segment [pos(a), pos(c)] intersects the obstacle and thus c will not appear in Sa.

Suppose that each obstacle is a polygon, described by a list of its vertices. A segment [pos(a), pos(b)] intersects the obstacle iff the segment intersects one of the segments of the polygon. Thus, testing intersection is done in polynomial time. Eventually, the model checking procedure can be adjusted to deal with obstacles and would remain in PSPACE.

The satisfiability testing problem now is modified as follows: given a set of obstacles positioned in the plane and a specification in BBL or any of its extensions, determine whether there is a positioning of the cameras in the plane (without moving the obstacles) such that the resulting configuration satisfies the specification. Its optimal complexity is currently under investigation.

Cameras in 3D

In the real world, cameras are usually placed in the 3D space and their areas of vision are 3-dimensional. That adds essential, though not crucial, technical overhead in computing the areas of vision of the cameras, but the logical languages and the epistemic parts of their semantics remain essentially unchanged. The model checking and satisfiability testing algorithms, without or with obstacles, can be suitably modified and will be in the same complexity classes as in 2D.

Moving cameras and robots

In reality the agents and their cameras are often mobile, not stationary. The simplest way to capture that feature is to consider the same logical languages over geometric models that only involve the agents and the vision angles of their cameras, but not their positions. Thus, the model checking problem for the case of mobile cameras, asking for suitable positioning of the cameras, satisfying the input specification, reduces to satisfiability testing problem for models with stationary cameras. A more refined approach for capturing mobile cameras involves adding to the language an extra dynamic operator for translations in the plane along the current direction of the camera. Together with the operator for rotations (turning) these can express every movement in the plane. The respective geometric models involve again only the sets of agents and the vision angles of their cameras, but not their positions. The possible worlds (states) in Kripke models and in their vision-based abstraction models remain the same. They are based on all sets of other agents that may be seen in a glance after any rotation and/or translation. In the recursive model checking procedure for the enriched languages, every occurrence of a translation operator in the formula applied to an agent a would generate a finite number of different model checking problems, arising by sliding the camera in the current direction of the agent a and only recording the changes occurring in the vision sets of the agents. Thus, eventually, the model checking problem for the case of mobile cameras can be reduced to repeated solving of finite sets of model checking problem for models with stationary cameras. The optimal complexity of the model checking problem with moving cameras is currently open.

Communicating agents with cameras

Lastly, the agents controlling cameras may have the ability of communicating with each other so that their respective knowledge can be broadcast to others. The interaction between knowledge and announcements has been studied and it is known that latter do not have negative effect on the complexity of the basic logic (see [START_REF] Lutz | Complexity and succinctness of public announcement logic[END_REF]). We conjecture that in our case, too, adding announcements would not increase the complexity of the model checking and satisfiability.

CONCLUDING REMARKS

We have introduced formal models for multi-agent systems, where agents control surveillance cameras, and logical languages to reason about the interaction between their vision and knowledge. The abstract scenario considered in this paper is applicable in principle to various real-life situations, ranging from systems of real-time surveillance cameras in building and public areas, through multi-robot systems, to networks of stationary satellites positioned around the globe. Thus, our framework and results have immediate potential applications to automated reasoning, formal specification and verification of observational abilities and knowledge of multi-agent systems in each of these situations.

Figure 1 :

 1 Figure 1: Two possible 2-dimensional worlds that are indistinguishable for agent a

Example 3 . 1 (

 31 Cameras and their sectors of vision).

•

  (pos, ang, D, R), dir |= a✄b iff pos(b) ∈ C pos(a),dir(a),ang(a) ; • (pos, ang, D, R), dir |= a φ iff there exists dir ′ ∈ Ra(dir) such that (pos, ang, D, R), dir ′ |= φ.

  3.2).Lemma 3.1. Given any Kripke structure M = (pos, ang, D, R), for every agent a we have that (≡ •Ra) = (Ra• ≡), where • is the composition of relations.

Example 3 . 2 .Proposition 3 . 2 .

 3232 In the geometrical model in Example 3.1 we have (trust us about the angles): • Sa = {∅, {b}, {b, d}, {b, d, e}, {d, e, c}, {e, c}, {c}}) • S b = {∅, {a}, {e}, {e, c}, {c, d}, {d}}; • Sc = {∅, {a}, {a, d}, {a, d, b}, {d, b}, {b, e}, {e}}; • S d = {∅, {a}, {b}, {e}, {e, c}, {c}}; • Se = {∅, {b}, {b, d}, {b, d, a}, {d, a}, {a}}. Each set Sa contains at most 2k -2 sets of agents, where k = (#Agt) is the number of agents. Hence so does the set Ra(dir) in the vision-based abstract model.

Proposition 3 . 3 .Corollary 3 . 2 .

 3332 The mapping h : KM → N defined by h(dir) = (Γ dir a ) a∈A is an isomorphism between the directionbased abstract model KM and the vision-based model N . For all formulas φ ∈ BBL, we have that KM, dir |= φ iff N, (Γ dir a ) a∈A |= φ.

Proposition 4 . 1 .

 41 Let N = (V, T ) be a vision-based abstraction model (def. 3.4), and v ∈ V , then: N, v |= φ iff N, v |= τ (φ).

Proposition 5 . 4 .

 54 SAT(BBLP DL) is PSPACE-hard. Proof. The formula ∃p1∀p2 . . . Qnpnψ(p1, . . . , pn) is true in QBL iff φ ′ is satisfiable where φ ′ = a1 [ a2] . . . Oiψ ′ where

Acknowledgements

The work of Valentin Goranko was partially supported by the CIMI (Centre International de Mathematiques et d'Informatique) Excellence program while in Toulouse as a scientific expert.


Thi Thao

Phuong Hoang
email: phuong.hoangthithao@inria.fr

Caroline Japhet
email: japhet@math.univ-paris13.fr

Michel Kern
email: michel.kern@inria.fr

Jean Roberts
email: jean.roberts@inria.fr

Ventcell conditions with mixed formulations for flow in porous media

Introduction

The Optimized Schwarz method has been introduced and analyzed over the last decade, where the convergence speed of the Jacobi iteration is significantly enhanced by using general transmission conditions on the interfaces together with optimized parameters. In particular, Ventcell transmission conditions (see Japhet [1998], [START_REF] Japhet | The Optimized Order 2 method. application to convection-diffusion problems[END_REF], [START_REF] Gander | Optimized Schwarz methods[END_REF], [START_REF] Dubois | Optimized Schwarz methods for the advection-diffusion equation and for problems with discontinuous coefficients[END_REF], [START_REF] Japhet | A new interface cement equilibrated mortar method with Ventcel conditions[END_REF], Halpern and Hubert, Gander et al.) have been studied for the primal formulation with different numerical schemes showing that the convergence of the Optimized Schwarz algorithm with Ventcell conditions is improved over that with Robin conditions. Ventcell conditions are second order differential conditions, see [START_REF] Ventcel | On boundary conditions for multi-dimensional diffusion processes[END_REF].

In this work, we study the Optimized Schwarz method with Ventcell conditions in the context of mixed formulations, which is not as straightforward as in the case of primal formulations and we have to introduce Lagrange multipliers on the interfaces to handle tangential derivatives involved in those conditions. Two dimensional numerical results for heterogeneous problems will be presented to compare the performance of the Ventcell transmission conditions with that of the Robin transmission conditions.

A model problem and domain decomposition with Ventcell transmission conditions

For an open, bounded domain Ω ⊂ R d (d = 2, 3) with Lipschitz boundary ∂Ω, consider single phase flow in a porous medium written in mixed form:

div u u u = f in Ω, K K K -1 u u u + ∇p = 0 in Ω, p = 0 on ∂Ω, (1)
where p is the pressure, u u u the Darcy velocity, f the source term and K K K a symmetric, positive definite, time independent, hydraulic conductivity (or permeability) tensor. For the sake of simplicity, we have imposed homogeneous Dirichlet condition on the boundary, other types of boundary conditions can be treated similarly. The well-posedness of problem ( 1) is well-known (see, e.g., [START_REF] Brezzi | On the existence, uniqueness and approximation of saddle-point problems arising from Lagrangian multipliers[END_REF], [START_REF] Brezzi | Mixed and hybrid finite elements methods[END_REF], Roberts and Thomas [1991]).

We consider a decomposition of Ω into two nonoverlapping subdomains, Ω 1 and Ω 2 , separated by an interface Γ :

Ω 1 ∩ Ω 2 = ∅; Γ = ∂Ω 1 ∩ ∂Ω 2 ∩ Ω, Ω = Ω 1 ∪ Ω 2 ∪ Γ.
Note that the same analysis can be extended to the case of many subdomains in bands. For i = 1, 2, let n n n i denote the unit, outward pointing, normal on ∂Ω i , and for any scalar, vector or tensor valued function ψ defined on Ω, let ψ i denote the restriction of ψ to Ω i . In order to write the Ventcell transmission conditions, we use the notation ∇ τ and div τ for the tangential gradient and divergence operators on Γ respectively. We denote by K K K i,Γ the tangential component of the trace of K K K i , i = 1, 2, on Γ . A multidomain formulation equivalent to problem (1) is obtained by solving in each subdomain the following problem div u u u

i = f in Ω i , K K K -1 i u u u i + ∇p i = 0 in Ω i , p i = 0 on (∂Ω i ∩ ∂Ω) , for i = 1, 2,
together with the transmission conditions

p 1 = p 2 , u u u 1 • n n n 1 + u u u 2 • n n n 2 = 0, on Γ. (2)
Under sufficient regularity, one may replace (2) by optimized Ventcell transmission conditions, which were introduced and analyzed for primal formulations in Japhet [1998], [START_REF] Japhet | The Optimized Order 2 method. application to convection-diffusion problems[END_REF]:

-u u u 1 • n n n 1 + α 1,2 p 1 + β 1,2 div τ (-K K K 2,Γ ∇ τ p 1 ) = -u u u 2 • n n n 1 + α 1,2 p 2 + β 1,2 div τ (-K K K 2,Γ ∇ τ p 2 ) on Γ, -u u u 2 • n n n 2 + α 2,1 p 2 + β 2,1 div τ (-K K K 1,Γ ∇ τ p 2 ) = -u u u 1 • n n n 2 + α 2,1 p 1 + β 2,1 div τ (-K K K 1,Γ ∇ τ p 1 ) on Γ, (3)
where α i,j and β i,j , i = 1, 2, j = (3i), are positive constants. The conditions (3) are derived in such a way that they are equivalent to the original ones given in (2) (cf. references above). These parameters are chosen to optimize the convergence factor, see Japhet [1998], [START_REF] Japhet | The Optimized Order 2 method. application to convection-diffusion problems[END_REF], [START_REF] Gander | Optimized Schwarz methods[END_REF], [START_REF] Dubois | Optimized Schwarz methods for the advection-diffusion equation and for problems with discontinuous coefficients[END_REF].

A multidomain formulation in mixed form

In this section, we study Ventcell transmission conditions with mixed formulations. In order to handle second order terms involved in (3), we introduce Lagrange multipliers on the interface Γ : p i,Γ , i = 1, 2, representing the pressure trace p i on Γ and a vector field

u u u Γ,i := -K K K j,Γ ∇ τ p i,Γ , i = 1, 2, j = (3-i).
We use the notation u u u Γ,i instead of u u u i,Γ to insist that u u u Γ,i is not the tangential component of the trace of u u u i on the interface. In fact u u u Γ,i is used as an artificial tool for convergence purposes (it does not have a particular physical meaning). We rewrite (3) defined on Γ as follows, for i = 1, 2, j = (3i):

-u u u i • n n n i + α i,j p i,Γ + β i,j div τ u u u Γ,i = -u u u j • n n n i + α i,j p j,Γ +β i,j div τ K K K j,Γ K K K -1 i,Γ u u u Γ,j , K K K -1 j,Γ u u u Γ,i + ∇ τ p i,Γ = 0.
(4)

The corresponding multidomain problem consists of solving in the subdomains the problem, for i = 1, 2, j = (3i):

div u u u i = f in Ω i , K K K -1 i u u u i + ∇p i = 0 in Ω i , p i = 0 on (∂Ω i ∩ ∂Ω) , -u u u i • n n n i + α i,j p i,Γ + β i,j div τ u u u Γ,i = -u u u j • n n n i + α i,j p j,Γ +β i,j div τ (K K K j,Γ K K K -1 i,Γ u u u Γ,j ) on Γ, K K K -1 j,Γ u u u Γ,i + ∇ τ p i,Γ = 0 on Γ, p i,Γ = 0 on ∂Γ.
(5) This can be seen as a coupling problem between a d-dimensional PDE in the subdomain Ω i and a (d -1)-dimensional PDE on the interface Γ , and both PDEs are written in mixed form. Under a suitable regularity hypothesis the multidomain problem ( 5) is equivalent to the monodomain problem (1). Details of the proof can be found in [Hoang, 2013, pp. 94 -95].

Well-posedness of the Ventcell local problem

For an open, bounded domain O ⊂ R d (d = 2, 3) with Lipschitz boundary ∂O, consider the following elliptic problem written in mixed form with Ventcell boundary conditions

div u u u O = f O in O, K K K -1 u u u O + ∇p O = 0 in O, -u u u O • n n n + αp ∂O + βdiv τ ũ u u ∂O = f ∂O on ∂O, K K K -1 ∂O ũ u u ∂O + ∇ τ p ∂O = 0 on ∂O, (6)
where n n n is the unit, outward pointing, normal vector on

∂O, K K K(•) ∈ R d 2 and K K K ∂O (•) ∈ R (d-1
) 2 are given, and α and β are positive constants. In order to write the weak formulation of problem (6), we define the following Hilbert spaces

M = µ = (µ O , µ ∂O ) ∈ L 2 (O) × L 2 (∂O) , Σ = v v v = (v v v O , ṽ v v ∂O ) ∈ L 2 (O) L 2 (O) L 2 (O) × L 2 (∂O) L 2 (∂O) L 2 (∂O) : div v v v O ∈ L 2 (O) and βdiv τ ṽ v v ∂O -v v v O • n n n |∂O ∈ L 2 (∂O) ,
equipped with the norms

µ 2 M = µ O 2 O + µ ∂O 2 ∂O , v v v 2 Σ = v v v O 2 O + div v v v O 2 O + ṽ v v ∂O 2 ∂O + βdiv ṽ v v ∂O -v v v O • n n n |∂O 2 ∂O ,
where • O and • ∂O are the L 2 (O) and L 2 (∂O)-norms, respectively. We denote by (•, •) O and (•, •) ∂O the inner products of L 2 (O) and L 2 (∂O).

Next, define the following bilinear forms (recall that β is a positive constant) on Σ × Σ, Σ × M and M × M respectively:

a(u u u, v v v) = K K K -1 u u u O , v v v O O + β K K K -1 ∂O ũ u u ∂O , ṽ v v ∂O ∂O , b(u u u, µ) = (div u u u O , µ O ) O + βdiv τ ũ u u ∂O -u u u O • n n n |∂O , µ ∂O ∂O , c(p, µ) = (αp ∂O , µ ∂O ) ∂O ,
and the linear form defined on M by:

L f (µ) = (f O , µ O ) O + (f ∂O , µ ∂O ) ∂O .
With these spaces and forms, the weak form of ( 6) can be written as follows:

Find (p, u u u) ∈ M × Σ such that a(u u u, v v v) -b(v v v, p) = 0 ∀v v v ∈ Σ, -b(u u u, µ) -c(p, µ) = -L f (µ) ∀µ ∈ M. ( 7
)
Theorem 1. Assume that there exist positive constants K -and

K + such that ς T K K K -1 (•)ς ≥ K -|ς| 2 , and |K K K(•)ς| ≤ K + |ς| a.e. in O and ∀ς ∈ R d ; and that η T K K K -1 ∂O (•)η ≥ K -|η| 2 , and | K K K ∂O (•)η| ≤ K + |η| a.e. in ∂O and ∀η ∈ R d-1 . If (f O , f ∂O ) is in M then there exists a unique solution (p, u u u) ∈ M × Σ of problem (7).
Proof. The existence and uniqueness of the solution of ( 7) is a generalization of the classical case (see [Brezzi and Fortin, 1991, pp. 47 -50], [Roberts and Thomas, 1991, pp. 572 -573]). See [Hoang, 2013, pp. 96 -98] for details of the proof of Theorem 1.

An interface problem

In this subsection, we derive an interface problem associated with the multidomain problem (5). With this aim, we define the Ventcell-to-Ventcell operator S VtV i (note that we have assumed sufficient regularity of the solution as in Section 2), which depends on the parameters α i,j and β i,j , for i = 1, 2, and j = (3i), as follows

S VtV i : L 2 (Γ ) × L 2 (Ω i ) → L 2 (Γ ) (ϑ, f ) -→ S VtV i (ϑ, f ) = -u u u i • n n n j|Γ + α j,i p i,Γ + β j,i div τ (K K K i,Γ K K K -1 j,Γ u u u Γ,i ), where (p i , u u u i , p i,Γ , u u u Γ,i ), i = 1, 2, is the solution of div u u u i = f in Ω i , K K K -1 i u u u i + ∇p i = 0 in Ω i , p i = 0 on (∂Ω i ∩ ∂Ω) , -u u u i • n n n i + α i,j p i,Γ + β i,j div τ u u u Γ,i = ϑ on Γ, K K K -1 j,Γ u u u Γ,i + ∇ τ p i,Γ = 0 on Γ, p i,Γ = 0 on ∂Γ. (8)
The well-posedness of problem ( 8) is given by an extension of Theorem 1. The interface problem, corresponding to the Ventcell transmission conditions (4), is defined by

ϑ 1 = S VtV 2 (ϑ 2 , f ) ϑ 2 = S VtV 1 (ϑ 1 , f ) on Γ, (9)
or equivalently,

S V S V S V ϑ 1 ϑ 2 = χ V χ V χ V (f ), on Γ, (10)
where

S V S V S V : L 2 (Γ ) × L 2 (Γ ) -→ L 2 (Γ ) × L 2 (Γ ) ϑ 1 ϑ 2 -→ ϑ 1 -S VtV 2 (ϑ 2 , 0) ϑ 2 -S VtV 1 (ϑ 1 , 0)
,

and χ V χ V χ V : L 2 (Γ ) -→ L 2 (Γ ) × L 2 (Γ ) f -→ S VtV 2 (0, f ) S VtV 1 (0, f ) .
One can solve problem (10) iteratively using Jacobi iteration or a Krylov method (e.g. GMRES, see for example [START_REF] Japhet | The Optimized Order 2 method. application to convection-diffusion problems[END_REF]) the right hand side is computed (only once) by solving problem (8) in each subdomain with ϑ = 0; then for a given pair of vectors (ϑ 1 , ϑ 2 ), the matrix vector product is obtained (at each iteration) by solving, for i = 1, 2, subdomain problem (8) in Ω i with ϑ = ϑ i and with f = 0. If one uses Jacobi iteration for solving (10), the resulting algorithm is equivalent to the optimized Schwarz algorithm with Ventcell transmission conditions (see Japhet [1998], [START_REF] Gander | Optimized Schwarz methods[END_REF]).

Numerical results

We consider a domain Ω = (0, π) 2 and its decomposition into two nonoverlapping subdomains Ω 1 = 0, π 2 × (0, π) and Ω 2 = π 2 , π × (0, π). The permeability is K K K = KI I I isotropic and constant on each subdomain, where I I I is the 2D identity matrix. We take K 1 = 1/K and K 2 = 1, where K = 1, 10 or 100. The exact solution is p(x, y) = cos(πx) sin(πy). For the spatial discretization, we use mixed finite elements (with interface Lagrange multipliers) with the lowest order Raviart-Thomas spaces on rectangles (see [START_REF] Brezzi | Mixed and hybrid finite elements methods[END_REF], Roberts and Thomas [1991]).

Remark 1. In order to handle the discontinuous coefficients, we use the optimized, weighted Ventcell parameters defined by

α 1,2 = K 2 α, α 2,1 = K 1 α, β 1,2 = K 2 β, β 2,1 = K 1 β.
The calculation of these parameters is done as in [START_REF] Dubois | Optimized Schwarz methods for the advection-diffusion equation and for problems with discontinuous coefficients[END_REF].

We first study the convergence behavior of the optimized Schwarz method with the optimized weighted Ventcell parameters. To that purpose, we con-sider the error equation, i.e. with f = 0 and homogeneous Dirichlet boundary conditions. We start with a random initial guess on the interface and compute the error in the L 2 (Ω)-norm of the pressure p and of the velocity u u u. Table 1 gives the number of iterations needed to reach an error reduction of 10 -6 first in p and then in u u u (in square brackets) as the mesh is refined. Both GMRES and Jacobi iterations are considered. For homogeneous case (K = 1), GMRES significantly improves the convergence speed (by a factor of 2) and also the asymptotic results compared to the Jacobi iteration. These results are consistent with those obtained with primal formulations in [START_REF] Gander | Optimized Schwarz methods[END_REF] (where a finite difference scheme is used). As the ratio K increases, the number of iterations is smaller and GMRES does not greatly accelerate the convergence speed compared to Jacobi iterations. Also for large values of the contrast K, the convergence rate of the algorithms with GMRES or Jacobi are almost independent of the mesh size (since the optimized parameters play the role of a preconditioner). This is also the case where a primal formulation and a finite volume method are used (cf. [START_REF] Dubois | Optimized Schwarz methods for the advection-diffusion equation and for problems with discontinuous coefficients[END_REF]). Next we verify the performance of the optimized parameters, computed by numerically minimizing the continuous convergence factor. We take h = π /100, vary α and β, and compute the error in the velocity u u u after a fixed number of Jacobi iterations for different permeability ratios. The results are shown in Figure 1 for K = 1 (# iter = 20 iterations), K = 10 (# iter = 12 iterations) and K = 100 (# iter = 8 iterations) respectively. We see that, in all cases, the optimized weighted Ventcell parameters (the red star) are located close to those giving the smallest error after the same number of iterations.

h K = 1 K = 10 K = 100 Jacobi GMRES Jacobi GMRES Jacobi GMRES π/
Finally, we illustrate the improvement obtained using Ventcell transmission conditions over the Robin conditions (i.e. β = 0).

We consider the optimized 2-sided Robin parameters with α 1,2 = α 2,1 and β 1,2 = β 2,1 = 0. Figures 2 shows the error in the pressure versus the number of iterations using Jacobi (on the left) and GMRES (on the right) for different diffusion ratios, K = 1 and K = 100 respectively.

We see that for the homogeneous case (K = 1), with Jacobi iterations the optimized weighted Ventcell converges significantly faster than the optimized 2-sided Robin (by a factor of 2). As K increases, the optimized weighted Ventcell and the optimized 2-sided Robin become comparable. With GMRES, the difference in the convergence of the two types of optimized parameters becomes less significant, especially for high diffusion ratios. These results are for a symmetric two subdomain case with a conforming mesh, Ventcell transmission conditions may have a more important effect on the convergence (compared with Robin transmission conditions) when many subdomains and nonmatching grids are considered (cf. [START_REF] Japhet | A new interface cement equilibrated mortar method with Ventcel conditions[END_REF]).

-6 -6 -5 -5 -5 -4 -4 -4 -4 -4 -3 -3 -3 -3 -3 -3 -3 -3 -2 -2 -2 -2 -2 -1 -1 -1 - 1

Fig. 1 Fig. 2 L

 12 Fig.1Level curves for the error in the velocity (in logarithmic scale) after some fixed number of Jacobi iterations for various values of the parameters α and β and for different permeability ratios K. The red star shows the optimized parameters.

Table 1

 1 Number of iterations required to reach an error reduction of 10 -6 in p and in u u u (in square brackets) for different permeability ratios, and for different values of the discretization parameter h.

	50 15 [15] 10 [11] 11 [10] 9 [9]	7 [6]	7 [7]
	π/100 17 [18] 11 [12] 11 [10] 9 [9]	7 [6]	7 [7]
	π/200 21 [21] 13 [13] 11 [10] 9 [9]	7 [6]	7 [7]
	π/400 25 [25] 14 [14] 11 [10] 10 [9]	7 [6]	8 [8]
	π/800 29 [29] 15 [16] 13 [12] 10 [10] 7 [6]	8 [8]

* This work was supported by ANDRA, the French Agency for Nuclear Waste Management. 1