BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Silvano Dal Zilio

Silvano Dal Zilio contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Logic in Computer ScienceSoftware EngineeringData Structures and AlgorithmsDistributed, Parallel, and Cluster Computing

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
9works
0followers
4topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

9 published item(s)

preprint2024arXiv

Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability

We propose a method for checking generalized reachability properties in Petri nets that takes advantage of structural reductions and that can be used, transparently, as a pre-processing step of existing model-checkers. Our approach is based on a new procedure that can project a property, about an initial Petri net, into an equivalent formula that only refers to the reduced version of this net. Our projection is defined as a variable elimination procedure for linear integer arithmetic tailored to the specific kind of constraints we handle. It has linear complexity, is guaranteed to return a sound property, and makes use of a simple condition to detect when the result is exact. Experimental results show that our approach works well in practice and that it can be useful even when there is only a limited amount of reductions.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Property Directed Reachability for Generalized Petri Nets

We propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the Property Directed Reachability (PDR) method. We actually define three different versions, that vary depending on the method used for abstracting possible witnesses, and that are able to handle problems of increasing difficulty. We have implemented our methods in a model-checker called SMPT and give empirical evidences that our approach can handle problems that are difficult or impossible to check with current state of the art tools.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Checking marking reachability with the state equation in Petri net subclasses

Although decidable, the marking reachability problem for Petri nets is well-known to be intractable in general, and a non-elementary lower bound has been recently uncovered. In order to alleviate this difficulty, various structural and behavioral restrictions have been considered, allowing to relate reachability to properties that are easier to check. For a given initial marking, the set of potentially reachable markings is described by the state equation solutions and over-approximates the set of reachable markings. In this paper, we delineate several subclasses of weighted Petri nets in which the set of reachable markings equals the set of potentially reachable ones, a property we call the PR-R equality. When fulfilled, this property allows to use linear algebra to answer the reachability questions, avoiding a brute-force analysis of the state space. Notably, we provide conditions under which this equality holds in classes much more expressive than marked graphs, adding places with several ingoing and outgoing transitions, which allows to model real applications with shared buffers. To achieve it, we investigate the relationship between liveness, reversibility, boundedness and potential reachability in Petri nets. We also show that this equality does not hold in classes with close modeling capability when the conditions are relaxed.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites

We propose a new approach for modelling the functional behaviour of an Earth observation satellite. We leverage this approach in order to develop a safety critical software, a "telecommand verifier", that is in charge of checking onboard whether a sequence of instructions is safe for execution. This new service is needed in order to add more autonomy to satellites. To do so, we propose a new Domain Specific Modelling Language and the toolchain required for integration into an embedded software. This framework is based on the composition of deterministic finite state machines with safety conditions , timeouts, and transitions that accept durations as a parameter. It is able to generate code in the synchronous programming language Lustre from a high-level specification of the satellite. This gives a formal way to derive an event-based algorithm simulating the execution of telecommand sequence and, thereupon, a provably correct onboard verifier.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

MCC: a Tool for Unfolding Colored Petri Nets in PNML Format

MCC is a tool designed for a very specific task: to transform the models of High-Level Petri nets, given in the PNML syntax, into equivalent Place/Transition nets. The name of the tool derives from the annual Model-Checking Contest, a competition of model-checking tools that provides a large and diverse collection of PNML models. This choice in naming serves to underline the main focus of the tool, which is to provide an open and efficient solution that lowers the access cost for developers wanting to engage in this competition. We describe the architecture and functionalities of our tool and show how it compares with other existing solutions. Despite the fact that the problem we target is abundantly covered in the literature, we show that it is still possible to innovate. To substantiate this assertion, we put a particular emphasis on two distinctive features of MCC that have proved useful when dealing with some of the most challenging colored models in the contest, namely the use of a restricted notion of higher-order invariant, and the support of a Petri net scripting language.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

On the Petri Nets with a Single Shared Place and Beyond

Petri nets proved useful to describe various real-world systems, but many of their properties are very hard to check. To alleviate this difficulty, subclasses are often considered. The class of weighted marked graphs with relaxed place constraint (WMG=< for short), in which each place has at most one input and one output, and the larger class of choice-free (CF) nets, in which each place has at most one output, have been extensively studied to this end, with various applications. In this work, we develop new properties related to the fundamental and intractable problems of reachability, liveness and reversibility in weighted Petri nets. We focus mainly on the homogeneous Petri nets with a single shared place (H1S nets for short), which extend the expressiveness of CF nets by allowing one shared place (i.e. a place with at least two outputs and possibly several inputs) under the homogeneity constraint (i.e. all the output weights of the shared place are equal). Indeed, this simple generalization already yields new challenging problems and is expressive enough for modeling existing use-cases, justifying a dedicated study. One of our central results is the first characterization of liveness in a subclass of H1S nets more expressive than WMG=< that is expressed by the infeasibility of an integer linear program (ILP) of polynomial size. This trims down the complexity to co-NP, contrasting with the known EXPSPACE-hardness of liveness in the more general case of weighted Petri nets. In the same subclass, we obtain a new reachability property related to the live markings, which is a variant of the well-known Keller&#39;s theorem. Another central result is a new reversibility characterization for the live H1S class, simplifying its checking. Finally, we apply our results to use-cases, highlight their scalability and discuss their extensibility to more expressive classes.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

A Verified Approach for Checking Real-Time Specification Patterns

We propose a verified approach to the formal verification of timed properties using model-checking techniques. We focus on properties expressed using real-time specification patterns, which can be viewed as a subset of timed temporal logics that includes properties commonly found during the analysis of reactive systems. Our model-checking approach is based on the use of observers in order to transform the verification of timed patterns into the verification of simpler LTL formulas. While the use of observers for model-checking is quite common, our contribution is original in several ways. First, we define a formal framework to verify that our observers are correct and non-intrusive. Second, we define different classes of observers for each pattern and use a pragmatic approach in order to select the most efficient candidate in practice. This approach is implemented in an integrated verification tool chain for the Fiacre language.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

An Experiment on Parallel Model Checking of a CTL Fragment

We propose a parallel algorithm for local, on the fly, model checking of a fragment of CTL that is well-suited for modern, multi-core architectures. This model-checking algorithm takes bene t from a parallel state space construction algorithm, which we described in a previous work, and shares the same basic set of principles: there are no assumptions on the models that can be analyzed; no restrictions on the way states are distributed; and no restrictions on the way work is shared among processors. We evaluate the performance of diff erent versions of our algorithm and compare our results with those obtained using other parallel model checking tools. One of the most novel contributions of this work is to study a space-e fficient variant for CTL model-checking that does not require to store the whole transition graph but that operates on a reverse spanning tree.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Real-Time Specification Patterns and Tools

An issue limiting the adoption of model checking technologies by the industry is the ability, for non-experts, to express their requirements using the property languages supported by verification tools. This has motivated the definition of dedicated assertion languages for expressing temporal properties at a higher level. However, only a limited number of these formalisms support the definition of timing constraints. In this paper, we propose a set of specification patterns that can be used to express real-time requirements commonly found in the design of reactive systems. We also provide an integrated model checking tool chain for the verification of timed requirements on TTS, an extension of Timed Petri Nets with data variables and priorities.

0 citations0 reviewsNo code linkedOpen access