arXiv subjects

Andrea Masini

Publications and source records attributed to Andrea Masini.

12 recordsLinked to original sources

arXiv2025

On Digital Twins in Defence: Overview and Applications

Digital twins have emerged as a transformative technology for modeling and simulation in various industries, including defense. This paper provides a comprehensive review of digital twin applications in defense modeling and simulation, focusing on how digital twins can enhance simulation fidelity, interoperability, and decision support within defense systems. We consolidate existing research into a unified framework that links digital twin concepts, simulation-driven application, and real-world deployment in defense scenarios. We discuss the role of digital twin in applications like planning, training, execution and monitoring, and debriefing. We introduce a standardized digital twin characterization framework suitable for defense application that aligns with industrial modeling and simulation standards, and present a taxonomy of defense specific use cases, highlighting recurring requirements. Additionally, practical evidence is provided from a targeted questionnaire distributed to defense stakeholders and Ministries of Defense, revealing current challenges in digital twin integration and deployment. Finally, we conclude by identifying key gaps in digital twins application for defense modeling and simulation, including interoperability, security, and system integration, and we outline future research directions and development opportunities. This review aims to inform defense modeling and simulation practitioners and researchers, guiding future work on digital twin design, implementation and deployment across defense applications.

cs.CR↗

arXiv2021

From 2-sequents and Linear Nested Sequents to Natural Deduction for Normal Modal Logics

We extend to natural deduction the approach of Linear Nested Sequents and of 2-sequents. Formulas are decorated with a spatial coordinate, which allows a formulation of formal systems in the original spirit of natural deduction -- only one introduction and one elimination rule per connective, no additional (structural) rule, no explicit reference to the accessibility relation of the intended Kripke models. We give systems for the normal modal logics from K to S4. For the intuitionistic versions of the systems, we define proof reduction, and prove proof normalization, thus obtaining a syntactical proof of consistency. For logics K and K4 we use existence predicates (following Scott) for formulating sound deduction rules.

cs.LO↗

arXiv2020

Quantum Turing Machines Computations and Measurements

Contrary to the classical case, the relation between quantum programming languages and quantum Turing Machines (QTM) has not being fully investigated. In particular, there are features of QTMs that have not been exploited, a notable example being the intrinsic infinite nature of any quantum computation. In this paper we propose a definition of QTM, which extends and unifies the notions of Deutsch and Bernstein and Vazirani. In particular, we allow both arbitrary quantum input, and meaningful superpositions of computations, where some of them are "terminated" with an "output", while others are not. For some infinite computations an "output" is obtained as a limit of finite portions of the computation. We propose a natural and robust observation protocol for our QTMs, that does not modify the probability of the possible outcomes of the machines. Finally, we use QTMs to define a class of quantum computable functions---any such function is a mapping from a general quantum state to a probability distribution of natural numbers. We expect that our class of functions, when restricted to classical input-output, will be not different from the set of the recursive functions.

cs.LO↗

arXiv2020

Real-Time target detection in maritime scenarios based on YOLOv3 model

In this work a novel ships dataset is proposed consisting of more than 56k images of marine vessels collected by means of web-scraping and including 12 ship categories. A YOLOv3 single-stage detector based on Keras API is built on top of this dataset. Current results on four categories (cargo ship, naval ship, oil ship and tug ship) show Average Precision up to 96% for Intersection over Union (IoU) of 0.5 and satisfactory detection performances up to IoU of 0.8. A Data Analytics GUI service based on QT framework and Darknet-53 engine is also implemented in order to simplify the deployment process and analyse massive amount of images even for people without Data Science expertise.

cs.CV↗

arXiv2020

A journey in modal proof theory: From minimal normal modal logic to discrete linear temporal logic

Extending and generalizing the approach of 2-sequents (Masini, 1992), we present sequent calculi for the classical modal logics in the K, D, T, S4 spectrum. The systems are presented in a uniform way-different logics are obtained by tuning a single parameter, namely a constraint on the applicability of a rule. Cut-elimination is proved only once, since the proof goes through independently from the constraints giving rise to the different systems. A sequent calculus for the discrete linear temporal logic ltl is also given and proved complete. Leitmotiv of the paper is the formal analogy between modality and first-order quantification.

cs.LO↗

arXiv2019

A two-dimensional metric temporal logic

We introduce a two-dimensional metric (interval) temporal logic whose internal and external time flows are dense linear orderings. We provide a suitable semantics and a sequent calculus with axioms for equality and extralogical axioms. Then we prove completeness and a semantic partial cut-elimination theorem down to formulas of a certain type.

math.LO↗

arXiv2015

Towards A Theory Of Quantum Computability

We propose a definition of quantum computable functions as mappings between superpositions of natural numbers to probability distributions of natural numbers. Each function is obtained as a limit of an infinite computation of a quantum Turing machine. The class of quantum computable functions is recursively enumerable, thus opening the door to a quantum computability theory which may follow some of the classical developments.

cs.LO↗

arXiv2009

A History of Until

Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: A until B holds at the current time instant w iff either B holds at w or there exists a time instant w' in the future at which B holds and such that A holds in all the time instants between the current one and w'. This "ambivalent" nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in contrast, we make explicit this duality of until to provide well-behaved natural deduction rules for linear-time logics by introducing a new temporal operator that allows us to formalize the "history" of until, i.e., the "internal" universal quantification over the time instants between the current one and w'. This approach provides the basis for formalizing deduction systems for temporal logics endowed with the until operator. For concreteness, we give here a labeled natural deduction system for a linear-time logic endowed with the new operator and show that, via a proper translation, such a system is also sound and complete with respect to the linear temporal logic LTL with until.

cs.LO↗

arXiv2009

Confluence Results for a Quantum Lambda Calculus with Measurements

A strong confluence result for Q*, a quantum lambda-calculus with measurements, is proved. More precisely, confluence is shown to hold both for finite and infinite computations. The technique used in the confluence proof is syntactical but innovative. This makes Q* different from similar quantum lambda calculi, which are either measurement-free or provided with a reduction strategy.

cs.LO↗

arXiv2008

A Qualitative Modal Representation of Quantum Register Transformations

We introduce two modal natural deduction systems that are suitable to represent and reason about transformations of quantum registers in an abstract, qualitative, way. Quantum registers represent quantum systems, and can be viewed as the structure of quantum data for quantum operations. Our systems provide a modal framework for reasoning about operations on quantum registers (unitary transformations and measurements), in terms of possible worlds (as abstractions of quantum registers) and accessibility relations between these worlds. We give a Kripke--style semantics that formally describes quantum register transformations and prove the soundness and completeness of our systems with respect to this semantics.

cs.LO↗

arXiv2007

Quantum Lambda Calculi with Classical Control: Syntax and Expressive Power

We study an untyped lambda calculus with quantum data and classical control. This work stems from previous proposals by Selinger and Valiron and by Van Tonder. We focus on syntax and expressiveness, rather than (denotational) semantics. We prove subject reduction, confluence and a standardization theorem. Moreover, we prove the computational equivalence of the proposed calculus with a suitable class of quantum circuit families.

cs.LO↗

arXiv2006

Continuations, proofs and tests

Continuation Passing Style (CPS) is one of the most important issues in the field of functional programming languages, and the quest for a primitive notion of types for continuation is still open. Starting from the notion of ``test'' proposed by Girard, we develop a notion of test for intuitionistic logic. We give a complete deductive system for tests and we show that it is good to deal with ``continuations''. In particular, in the proposed system it is possible to work with Call by Value and Call by Name translations in a uniform way.

cs.LO↗