Researcher profile

Lorenzo Capra

Lorenzo Capra contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate

Trust snapshot

Quick read

Trust 17 - UnverifiedVerification L1Unclaimed author
4works
0followers
6topics
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

4 published item(s)

preprint2020arXiv

Multiple Sclerosis disease: a computational approach for investigating its drug interactions

Multiple Sclerosis (MS) is a chronic and potentially highly disabling disease that can cause permanent damage and deterioration of the central nervous system. In Europe it is the leading cause of non-traumatic disabilities in young adults, since more than 700,000 EU people suffer from MS. Although recent studies on MS pathophysiology have been provided, MS remains a challenging disease. In this context, thanks to recent advances in software and hardware technologies, computational models and computer simulations are becoming appealing research tools to support scientists in the study of such disease. Thus, motivated by this consideration we propose in this paper a new model to study the evolution of MS in silico, and the effects of the administration of Daclizumab drug, taking into account also spatiality and temporality of the involved phenomena. Moreover, we show how the intrinsic symmetries of the system can be exploited to drastically reduce the complexity of its analysis.

preprint2013arXiv

Distributed CTL Model Checking in the Cloud

The recent extensive availability of "big data" platforms calls for a more widespread adoption by the formal verification community. In fact, formal verification requires high performance data processing software for extracting knowledge from the unprecedented amount of data which come from analyzed systems. Since cloud based computing resources have became easily accessible, there is an opportunity for verification techniques and tools to undergo a deep technological transition to exploit the new available architectures. This has created an increasing interest in parallelizing and distributing verification techniques. In this paper we introduce a distributed approach which exploits techniques typically used by the "big data" community to enable verification of Computation Tree Logic (CTL) formulas on very large state spaces using distributed systems and cloud computing facilities. The outcome of several tests performed on benchmark specifications are presented, thus showing the convenience of the proposed approach.

preprint2012arXiv

State Space Exploration of RT Systems in the Cloud

The growing availability of distributed and cloud computing frameworks make it possible to face complex computational problems in a more effective and convenient way. A notable example is state-space exploration of discrete-event systems specified in a formal way. The exponential complexity of this task is a major limitation to the usage of consolidated analysis techniques and tools. We present and compare two different approaches to state-space explosion, relying on distributed and cloud frameworks, respectively. These approaches were designed and implemented following the same computational schema, a sort of map & fold. They are applied on symbolic state-space exploration of real-time systems specified by (a timed extension of) Petri Nets, by readapting a sequential algorithm implemented as a command-line Java tool. The outcome of several tests performed on a benchmarking specification are presented, thus showing the convenience of cloud approaches.

preprint2011arXiv

Reachability Analysis of Time Basic Petri Nets: a Time Coverage Approach

We introduce a technique for reachability analysis of Time-Basic (TB) Petri nets, a powerful formalism for real- time systems where time constraints are expressed as intervals, representing possible transition firing times, whose bounds are functions of marking's time description. The technique consists of building a symbolic reachability graph relying on a sort of time coverage, and overcomes the limitations of the only available analyzer for TB nets, based in turn on a time-bounded inspection of a (possibly infinite) reachability-tree. The graph construction algorithm has been automated by a tool-set, briefly described in the paper together with its main functionality and analysis capability. A running example is used throughout the paper to sketch the symbolic graph construction. A use case describing a small real system - that the running example is an excerpt from - has been employed to benchmark the technique and the tool-set. The main outcome of this test are also presented in the paper. Ongoing work, in the perspective of integrating with a model-checking engine, is shortly discussed.