Nicola Gigante

Free University of Bozen-Bolzano

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Trends

Author Order

Document Type

Co-Authors

Luca Geatti

University of Udine

Angelo Montanari

University of Udine

Alessandro Cimatti

Fondazione Bruno Kessler

Stefano Tonetta

Fondazione Bruno Kessler

Mark Reynolds

University of Western Australia

Angelo Montanari

University of Udine

Marta Cialdea Mayer

Roma Tre University

Andrea Orlandini

Institute of Cognitive Sciences and Technologies

Alessandro Gianola

Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento

Renato Acampora

University of Udine

Cooperative Institutions

University of Udine

Free University of Bozen-Bolzano

Fondazione Bruno Kessler

University of Trento

TU Dresden

Universidad Complutense de Madrid

Sapienza University of Rome

TU Wien

Politecnico di Milano

University of Parma

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Field

Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL+P Synthesis

Lecture notes in computer science (2021)

Alessandro Cimatti Luca Geatti Nicola Gigante Angelo Montanari Stefano Tonetta

Realizability

Soundness

Completeness (order theory)

10.1007/978-3-030-92124-8_20

Cite

Citations (1)

A first-order logic characterization of safety and co-safety languages

arXiv (Cornell University) (2022)

Alessandro Cimatti Luca Geatti Nicola Gigante Angelo Montanari Stefano Tonetta

Linear Temporal Logic (LTL) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Among the various reasons of its widespread use there are its strong foundational properties: LTL is equivalent to counter-free omega-automata, to star-free omega-regular expressions, and (by Kamp's theorem) to the First-Order Theory of Linear Orders (FO-TLO). Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not belong or belongs to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for LTL. SafetyLTL (resp., coSafetyLTL) is a fragment of LTL where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. The main contribution of this paper is the introduction of a fragment of FO-TLO, called SafetyFO, and of its dual coSafetyFO, which are expressively complete with respect to the LTL-definable safety and co-safety languages. We prove that they exactly characterize SafetyLTL and coSafetyLTL, respectively, a result that joins Kamp's theorem, and provides a clearer view of the characterization of (fragments of) LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in LTL is definable in SafetyLTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of SafetyLTL, interpreted over finite and infinite words. Moreover, we prove that, when interpreted over finite words, SafetyLTL (resp. coSafetyLTL) devoid of the tomorrow (resp., weak tomorrow) operator captures the safety (resp., co-safety) fragment of LTL over finite words.

Fragment (logic)

Regular language

Characterization

10.48550/arxiv.2209.02307

Cite

Citations (1)

GR(1) is equivalent to R(1)

Information Processing Letters (2022)

Alessandro Cimatti Luca Geatti Nicola Gigante Angelo Montanari Stefano Tonetta

Reactivity

Lift (data mining)

Basis (linear algebra)

10.1016/j.ipl.2022.106319

Cite

Citations (0)

SMT-Based Symbolic Model-Checking for Operator Precedence Languages

Lecture notes in computer science (2024)

Michele Chiari Luca Geatti Nicola Gigante Matteo Pradella

Operator (biology)

10.1007/978-3-031-65627-9_19

Cite

Citations (1)

BLACK: A Fast, Flexible and Reliable LTL Satisfiability Checker.

Luca Geatti Nicola Gigante Angelo Montanari

Satisfiability

Source

Cite

Citations (6)

Extended bounded response LTL: a new safety fragment for efficient reactive synthesis

Formal Methods in System Design (2021)

Alessandro Cimatti Luca Geatti Nicola Gigante Angelo Montanari Stefano Tonetta

Fragment (logic)

Büchi automaton

10.1007/s10703-021-00383-3

Cite

Citations (8)

Inferring Markov Chains to Describe Convergent Tumor Evolution With CIMICE

IEEE/ACM Transactions on Computational Biology and Bioinformatics (2023)

N. Rossi Nicola Gigante Nicola Vitacolonna Carla Piazza

The field of tumor phylogenetics focuses on studying the differences within cancer cell populations. Many efforts are done within the scientific community to build cancer progression models trying to understand the heterogeneity of such diseases. These models are highly dependent on the kind of data used for their construction, therefore, as the experimental technologies evolve, it is of major importance to exploit their peculiarities. In this work we describe a cancer progression model based on Single Cell DNA Sequencing data. When constructing the model, we focus on tailoring the formalism on the specificity of the data. We operate by defining a minimal set of assumptions needed to reconstruct a flexible DAG structured model, capable of identifying progression beyond the limitation of the infinite site assumption. Our proposal is conservative in the sense that we aim to neither discard nor infer knowledge which is not represented in the data. We provide simulations and analytical results to show the features of our model, test it on real data, show how it can be integrated with other approaches to cope with input noise. Moreover, our framework can be exploited to produce simulated data that follows our theoretical assumptions. Finally, we provide an open source R implementation of our approach, called CIMICE, that is publicly available on BioConductor.

Bioconductor

Formalism (music)

10.1109/tcbb.2023.3337258

Cite

Citations (0)

Complexity of Safety and coSafety Fragments of Linear Temporal Logic

arXiv (Cornell University) (2022)

Alessandro Artale Luca Geatti Nicola Gigante Andrea Mazzullo Angelo Montanari

Linear Temporal Logic (LTL) is the de-facto standard temporal logic for system specification, whose foundational properties have been studied for over five decades. Safety and cosafety properties define notable fragments of LTL, where a prefix of a trace suffices to establish whether a formula is true or not over that trace. In this paper, we study the complexity of the problems of satisfiability, validity, and realizability over infinite and finite traces for the safety and cosafety fragments of LTL. As for satisfiability and validity over infinite traces, we prove that the majority of the fragments have the same complexity as full LTL, that is, they are PSPACE-complete. The picture is radically different for realizability: we find fragments with the same expressive power whose complexity varies from 2EXPTIME-complete (as full LTL) to EXPTIME-complete. Notably, for all cosafety fragments, the complexity of the three problems does not change passing from infinite to finite traces, while for all safety fragments the complexity of satisfiability (resp., realizability) over finite traces drops to NP-complete (resp., ${\Pi}^P_2$-complete).

Realizability

Satisfiability

TRACE (psycholinguistics)

Boolean satisfiability problem

Expressive power

Prefix

10.48550/arxiv.2211.14913

Cite

Citations (0)

Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker

International Symposium on Temporal Representation and Reasoning (2021)

Luca Geatti Nicola Gigante Angelo Montanari Gabriele Venturato

LTL+Past is the extension of Linear Temporal Logic (LTL) supporting past temporal operators. The addition of the past does not add expressive power, but does increase the usability of the language both in formal verification and in artificial intelligence, e.g., in the context of multi-agent systems. In this paper, we add the support of past operators to BLACK, a satisfiability checker for LTL based on a SAT encoding of a tree-shaped tableau system. We implement two ways of supporting the past in the tool. The first one is an equisatisfiable translation that removes the past operators, obtaining a future-only formula that can be solved with the original LTL engine. The second one extends the SAT encoding of the underlying tableau to directly support the tableau rules that deal with past operators. We describe both approaches and experimentally compare the two between themselves and with the νXmv model checker, obtaining promising results.

Satisfiability

Fragment (logic)

Boolean satisfiability problem

10.4230/lipics.time.2021.8

Cite

Citations (2)

Synthesis of Timeline-Based Planning Strategies Avoiding Determinization

Electronic Proceedings in Theoretical Computer Science (2024)

Renato Acampora Dario Della Monica Luca Geatti Nicola Gigante Angelo Montanari

Qualitative timeline-based planning models domains as sets of independent, but interacting, components whose behaviors over time, the timelines, are governed by sets of qualitative temporal constraints (ordering relations), called synchronization rules. Its plan-existence problem has been shown to be PSPACE-complete; in particular, PSPACE-membership has been proved via reduction to the nonemptiness problem for nondeterministic finite automata. However, nondeterministic automata cannot be directly used to synthesize planning strategies as a costly determinization step is needed. In this paper, we identify a large fragment of qualitative timeline-based planning whose plan-existence problem can be directly mapped into the nonemptiness problem of deterministic finite automata, which can then be exploited to synthesize strategies. In addition, we identify a maximal subset of Allen's relations that fits into such a deterministic fragment.

Time line

10.4204/eptcs.409.5

Cite

Citations (0)