Structured Proofs for Adversarial Cyber-Physical Systems

Many cyber-physical systems (CPS) are safety-critical, so it is important to formally verify them, e.g. in formal logics that show a model’s correctness specification always holds. Constructive Differential Game Logic ( CdGL ) is such a logic for (constructive) hybrid games, including hybrid systems. To overcome undecidability, the user first writes a proof, for which we present a proof-checking tool. We introduce Kaisar , the first language and tool for CdGL proofs, which until now could only be written by hand with a low-level proof calculus. Kaisar’s structured proofs simplify challenging CPS proof tasks, especially by using programming language principles and high-level stateful reasoning. Kaisar exploits CdGL ’s constructivity and refinement relations to build proofs around models of game strategies. The evaluation reproduces and extends existing case studies on 1D and 2D driving. Proof metrics are compared and reported experiences are discussed for the original studies and their reproductions.

A Method to Develop Virtual Reality Platforms for the Medical Rehabilitation of Severe Memory Loss After Brain Stroke

The paper presents a method to develop Virtual Reality (VR) platforms based on serious games for the rehabilitation of severe memory loss. In particular, it is related to retrograde amnesia, a condition affecting patient’s quality of life usually caused by brain stroke. Nowadays, the standard rehabilitation process consists in showing pictures of patient’s familiar environments in order to recover the memory. Past research works have investigated the use of 3D scanners for the virtualization of real environment and virtual reality for the generation of more immersive interaction to design serious games for neurocognitive rehabilitation. Reached results highlighted a time-consuming development process to interface each new environment with the game logic specifically developed for the serious games. Furthermore, a complete VR platform must also consider the medical monitoring and the data management oriented to a more objective medical assessment. The proposed method allows the design of VR platforms based on patient-specific serious games for memory loss starting from the 3D scanning acquisition of familiar environments. The 3D acquisition is performed using the Occipital Structure Sensor and the Skanect application. A modular procedure has been designed to interface the virtual objects of each acquired environment with the modules of the game-logic developed with Unity. The immersive Virtual Reality is based on the use of the HTC Vive Pro head mounted display. Furthermore, the method permits to associate the patient-specific serious game to a set of software modules for the medical monitoring and the data management for the generation of reports useful for the evaluation. The solution has been evaluated by measuring the time needed to develop a whole VR platform for two different familiar environments. Less than 5 hours are required to complete the design process.

‘They have to help themselves’: Saw and the horrors of neo-liberalism

Critical examinations of the Saw films have generally focused on their post-9/11 production context and the link between the War on Terror and images of spectacular violence. This article argues that Saw and its sequels can instead fruitfully be understood as products of new neo-liberal regimes of subjecthood. As neo-liberal ideology and policy push market logics further into everyday lives, new forms of immaterial labour force the worker to act both as disciplining manager and as disciplined worker. By tracing neo-liberal subjectivity’s emphasis on individualized agency and responsibility through Jigsaw’s ideology, this piece shows that Saw dramatizes the parody of freedom offered by late capitalism. Jigsaw, like neo-liberalism itself, operates through a complex assemblage of technology, ethics and guilt, which forces the neo-liberal subject to enact its own punishment. Saw’s trademark traps are explored through the series’ use of video game logic and language in order to position Jigsaw’s victims within the more subtle mechanisms of control necessitated by contemporary capitalism.

Constructive Game Logic

Game Logic is an excellent setting to study proofs-about-programs via the interpretation of those proofs as programs, because constructive proofs for games correspond to effective winning strategies to follow in response to the opponent’s actions. We thus develop Constructive Game Logic, which extends Parikh’s Game Logic (GL) with constructivity and with first-order programs à la Pratt’s first-order dynamic logic (DL). Our major contributions include: 1. a novel realizability semantics capturing the adversarial dynamics of games, 2. a natural deduction calculus and operational semantics describing the computational meaning of strategies via proof-terms, and 3. theoretical results including soundness of the proof calculus w.r.t. realizability semantics, progress and preservation of the operational semantics of proofs, and Existential Properties on support of the extraction of computational artifacts from game proofs. Together, these results provide the most general account of a Curry-Howard interpretation for any program logic to date, and the first at all for Game Logic.

Cloudification of Virtual Reality Gliding Simulation Game

Cloud gaming provides cloud computing-based game as a service. In this paper we describe the development of a virtual reality base gliding game as a proof-of-concept. In the cloud, a cloud gaming platform is hosted on cloud servers with two principal components: game logic engaged in the implementation of game mechanics and game interactions, and video renderer that generates the game frames in real-time. The virtual gliding game was realized in the Unity gaming engine. To ensure smooth playability, and access for remote players, the computationally-intensive parts of the game were offloaded to a physically remote cloud server. To analyze the efficiency of the client-cloud interaction, three cloud servers were setup. The results of cloudification were evaluated by measuring and comparing computation offloading performance, network traffic, the probability of service drop, perceptual quality and video quality.

Maps, Improvisation, and Games: Retaining Biblical Authority in Local Theology

One of the primary tasks of local theology is to address questions and challenges that are context-specific but not explicitly addressed in the Bible. How can biblical authority be retained while attempting to answer questions, whereby the theologian is compelled to go beyond explicit biblical teaching? Ways of resolving the seeming tension between local theologizing and the normative authority of Scripture are addressed by examining three somewhat novel approaches to conceptualizing the theological process. The first is Paul G. Hiebert’s idea of critical realism and the analogy of maps. The second is Kevin J. Vanhoozer’s idea of theodrama and improvisation. The third is my own concept of game logic and strategy. Each of these three conceptualizations will be briefly described with particular attention to the task of local theologizing and biblical authority.