Abstract We introduce a hybrid spatiotemporal logic for automotive safety applications (HSTL), focused on highway driving. Spatiotemporal logic features specifications about vehicles throughout space and time, while hybrid logic enables precise references to individual vehicles and their historical positions. We define the semantics of HSTL and provide a baseline model-checking algorithm for it. We propose two optimized model-checking algorithms, which reduce the search space based on the reachable states and possible transitions from one state to another. All three model-checking algorithms are evaluated on a series of common driving scenarios such as safe following, safe crossings, overtaking, and platooning. An exponential performance improvement is observed for the optimized algorithms.

While normative - "good"- game design and user experiences have been established, we look to games that challenge those notions. Intentional frustration and failure can be worthwhile. Through a reflexive thematic analysis of 31 games we identify how intentionally non-normative design choices lead to meaningful experiences. Working within the established Mechanics Dynamics Aesthetics (MDA) Game Design Framework, we lay out themes to design Shitty User Experiences (SUX). We contribute SUX MDA themes for designers and researchers to counter the status quo and identify new forms of play and interaction.

Many transgender (and cisgender) people experience gender euphoria - satisfaction and relief caused by self-actualization and gender congruence - a term that has been overlooked by the design community. Video games create intense experiences involving identities, bodies, and social interaction, providing opportunities to empower people through gender euphoria. We develop themes for creating and supporting gender euphoria in games within the Design, Dynamics, Experience Game Design Framework from a reflexive thematic analysis of 25 games, with an in-depth analysis of four of them. The analysis combines the authors' positionalities as trans gamers with close reading and content analysis of the games, employing perspectives from critical discourse analysis. We contribute an operational understanding of gender euphoria to support design, in-depth case studies of particularly euphoric game experiences, and identify themes that designers and researchers can use to develop new games and analyze existing ones.

Many trans people experience marginalization and violence in cyberspace. This violence is characterized by intricate dynamics surrounding voice, identities, bodies, and social interactions. To comprehend and provide a theoretical framework for this enduring phenomenon of digital violence, the present research introduces the concept of Trans Cyber-Necropolitics (TCN). TCN is a necropolitical system that explains how digital media enforce the disposability of trans people in cyberspace. We decompose this digital death into three steps: sensing , targeting , and invisible killing . Combining with the authors’ positionality as transgender gamers, we provide a critical analysis of how each step operates, conducted via a meticulous examination of games, as well as an exploration of the discourse from game design and community-side comments through the lens of critical discourse analysis. Building on this analysis, we ideate how each step could be disrupted with resistance strategies and technological measures.

This paper presents Neurotype Cafe, a visual novel video game about a young autistic woman with ADHD, Nia, who works in a cafe. Originally developed as a student capstone project, Neurotype Cafe serves as a case study in neurodiverse self-representation, i.e., how neurodiverse development teams can integrate their lived experience with their professional expertise to develop play experiences that center neurodiverse audiences. The game explores themes of self-acceptance, anti-perfectionism, and bridging communication gaps between different ways of experiencing the world, centering Nia’s perspective. The primary goal of this game is to depict everyday experiences of neurodivergent people through both narrative events and game mechanics which center neurodivergent audiences without foreclosing neurotypical ones. The game received a best project award from program faculty.

We introduce a goal-aware extension of responsibility-sensitive safety (RSS), a recent methodology for rule-based safety guarantee for automated driving systems (ADS). Making RSS rules guarantee goal achievement—in addition to collision avoidance as in the original RSS—requires complex planning over long sequences of manoeuvres. To deal with the complexity, we introduce a compositional reasoning framework based on program logic, in which one can systematically develop RSS rules for smaller subscenarios and combine them to obtain RSS rules for bigger scenarios. As the basis of the framework, we introduce a program logic dFHL that accommodates continuous dynamics and safety conditions. Our framework presents a dFHL-based workflow for deriving goal-aware RSS rules; we discuss its software support, too. We conducted experimental evaluation using RSS rules in a safety architecture. Its results show that goal-aware RSS is indeed effective in realising both collision avoidance and goal achievement.

Many trans people experience gender dysphoria -- distress caused by mismatches in internal and external experiences of gender. Video games engage intimately with the self, creating intense experiences involving identities, bodies, and social interaction. This combination of factors renders trans players vulnerable to gender dysphoria triggers: failures of interaction design that result in gender dysphoria. The present research undertakes a thematic analysis of four popular games, drawn from an initial corpus of 31. It contributes a definition of gender dysphoria triggers, case studies of triggering games, an initial gender dysphoria categorization to provide a useful design language, and examples of alternative designs for extant triggers. The analysis combines the authors' positionality as trans gamers; critical cultural studies methodologies, including textual analysis; a critical discourse analysis of production-side statements and interviews and player-side comments about diversity in those games; and close readings of the games themselves. The paper concludes with a call for trans inclusivity in game design, which we structure around the necropolitical concept of the relation of care.

Intermittently powered embedded systems are a foundational and growing component of the Internet of Things. It is essential to rigorously prove these systems’ correctness because they arise both in safety-critical applications and applications where quality-of-service is essential to social good. Such proofs are challenging because they are simultaneously cyber–physical and time-sensitive: correctness is affected by physical properties that change with time. This article introduces a new general-purpose formal verification approach for cyber–physical properties of intermittent systems. We define a high-level modeling and specification language for intermittent systems, define its formal semantics, and prove that the language reduces to hybrid games, enabling the application of existing theorem-proving software. Cold storage for COVID vaccines serves as a running example; we provide a machine-checked proof that safe temperatures are maintained under suitable assumptions. The crux of our proof approach is to identify power and timing assumptions under which sufficient power is available to complete time-sensitive tasks. Orthogonal to approaches that prove new guarantees on power or timing, our work rigorously shows which power and timing assumptions are needed for cyber–physical correctness.

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.

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

We extend the constructive differential game logic (CdGL) of hybrid games with a refinement connective that relates two hybrid games. In addition to CdGL’s ability to prove the existence of winning strategies for specific postconditions of hybrid games, game refinements relate two games to one another. That makes it possible to prove that any winning strategy for any postcondition of one game carries over to a winning strategy for the other. Since CdGL is constructive, a computable winning strategy can be extracted from a proof that a player wins a game. A folk theorem says that any such winning strategy for a hybrid game gives rise to a corresponding hybrid system satisfying the same property. We make this precise using CdGL’s game refinements and prove correct the construction of hybrid systems from winning strategies of hybrid games.

Information-flow security is important to the safety and privacy of cyber-physical systems (CPSs) across many domains: information leakage can both violate user privacy and reveal vulnerabilities to physical attacks. CPSs face the challenge that information can flow both in discrete cyber channels and in continuous real-valued physical channels ranging from time to motion to electrical currents. We call these hybrid-dynamic information flows (HDIFs) and introduce dHL, the first logic for verifying HDIFs in hybrid-dynamical models of CPSs. Our logic extends differential dynamic logic (dL) for hybrid-dynamical systems with hybrid-logical features for explicit program state representation, supporting relational reasoning used for information flow arguments. By verifying HDIFs, we ensure security even under a strong attacker model wherein an attacker can observe time and physical values continuously. We present a Hilbert-style proof calculus for dHL, prove it sound, and compare the expressive power of dHL with dL. We develop a hybrid system model based on the smart electrical grid FREEDM, with which we showcase dHL. We prove that the naive model has a previously unknown information flow vulnerability, which we verify is resolved in a revised model. This is the first information flow proof both for HDIFs and for a hybrid-dynamical model in general.

We present VeriPhy, a verified pipeline which automatically transforms verified high-level models of safety-critical cyber-physical systems (CPSs) in differential dynamic logic (dL) to verified controller executables. VeriPhy proves that all safety results are preserved end-to-end as it bridges abstraction gaps, including: i) the gap between mathematical reals in physical models and machine arithmetic in the implementation, ii) the gap between real physics and its differential-equation models, and iii) the gap between nondeterministic controller models and machine code. VeriPhy reduces CPS safety to the faithfulness of the physical environment, which is checked at runtime by synthesized, verified monitors. We use three provers in this effort: KeYmaera X, HOL4, and Isabelle/HOL. To minimize the trusted base, we cross-verify KeYmaeraX in Isabelle/HOL. We evaluate the resulting controller and monitors on commodity robotics hardware.

We formalize the soundness theorem for differential dynamic logic, a logic for verifying hybrid systems. To increase confidence in the formalization, we present two versions: one in Isabelle/HOL and one in Coq. We extend the metatheory to include features used in practice, such as systems of differential equations and functions of multiple arguments. We demonstrate the viability of constructing a verified kernel for the hybrid systems theorem prover KeYmaera X by embedding proof checkers for differential dynamic logic in Coq and Isabelle. We discuss how different provers and libraries influence the design of the formalization.