Arrow Research search

Author name cluster

Thomas Studer

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers
2 author rows

Possible papers

8

TCS Journal 2025 Journal Article

Synergistic knowledge

  • Christian Cachin
  • David Lehnherr
  • Thomas Studer

Simplicial complexes are a successful model for distributed computing. They have recently been observed to provide an interesting model for epistemic multi-agent logic where the agents' local states are the main building blocks (instead of the global states). A natural generalization is to study epistemic logic on semi-simplicial sets. However, finding the appropriate modal logic for semi-simplicial models has been an open question. We answer this by introducing the logic of synergistic knowledge and establishing its soundness and completeness.

Details DOI

FormaliSE Conference 2025 Conference Paper

Temporal Logics Meet Real-World Software Requirements: A Reality Check

  • Roman Bögli
  • Atefeh Rohani
  • Thomas Studer
  • Christos Tsigkanos
  • Timo Kehrer

Reasoning on the behavior of software systems is challenging, especially in critical domains such as aerospace. Transitioning from natural language to formal specifications enables long-pursued activities such as modeling, synthesis, and verification. Temporal logics are often used in this regard, each with different operators, expressiveness or associated implementations. However, a significant gap exists between the theoretical capabilities of the logics applied in formal methods and the practical needs for specifying real-world requirements. This paper addresses this gap through a case study of SpaceWire, a standard specification for a data-handling communication protocol often adopted on spacecraft and other on-board systems. We extract 89 software requirements exhibiting temporal behavior and transcribe them into logic-based formalizations using different established temporal logics, maximizing natural encoding. We analyze the suitability of the chosen logics for formalizing the selected software requirements to reason about potential implications for both researchers and practitioners.

Details

AAMAS Conference 2023 Conference Paper

What Do You Care About: Inferring Values from Emotions

  • Jieting Luo
  • Mehdi Dastani
  • Thomas Studer
  • Beishui Liao

Observers can glean information from others’ emotional expressions through the act of drawing inferences from another individual’s emotional expressions. It is important for socially aware artificial systems to be capable of doing that as it can facilitate social interaction among agents, and is particularly important in humanrobot interaction for supporting a more personalized treatment of users. In this short paper, we propose a methodology for developing a formal model that allows agents to infer another agent’s values from her emotion expressions.

PDF

FLAP Journal 2019 Journal Article

Relevant Justification Logic.

  • Nenad Savic
  • Thomas Studer

We introduce a relevant justification logic, RJ4, which is a combination of the relevant logic R and the justification logic J4. We describe the corresponding class of models, provide the axiomatization and prove that our logic is sound and complete.

Details

LORI Conference 2017 Conference Paper

Justification Logic with Approximate Conditional Probabilities

  • Zoran Ognjanovic
  • Nenad Savic
  • Thomas Studer

Abstract The importance of logics with approximate conditional probabilities is reflected by the fact that they can model non-monotonic reasoning. We introduce a new logic of this kind, \(\mathsf {CPJ}\), which extends justification logic and supports non-monotonic reasoning with and about evidences.

Details

FLAP Journal 2016 Journal Article

Intuitionistic Modal Logic made Explicit.

  • Michel Marti
  • Thomas Studer

The logic of proofs of Heyting arithmetic includes explicit justifications for all admissible rules of intuitionistic logic in order to satisfy completeness with respect to provability semantics. We study the justification logic iJT4, which does not have these additional justification terms. We establish that iJT4 is complete with respect to modular models, which provide a Kripke-style seman- tics, and that there is a realization of intuitionistic S4 into iJT4. Hence iJT4 can be seen as an explicit version of intuitionistic S4.

PDF Details

TCS Journal 2001 Journal Article

How to normalize the Jay

  • Dieter Probst
  • Thomas Studer

In this note we give an elementary proof of the strong normalization property of the J combinator by providing an explicit bound for the maximal length of the reduction paths of a term. This result shows clearly that in the theorem of Toyama, Klop and Barendregt on completeness of unions of left-linear term rewriting systems, disjointness is essential.

Details DOI

CSL Conference 2000 Conference Paper

A Theory of Explicit Mathematics Equivalent to ID 1

  • Reinhard Kahle
  • Thomas Studer

Abstract We show that the addition of name induction to the theory \( EETJ + \left( {\mathcal{L}_{EM} - I_N } \right) \) of explicit elementary types with join yields a theory proof-theoretically equivalent to ID 1.

Details