7 Search Results for "Cardelli, Luca"

Document
DOI: 10.4230/LIPIcs.CONCUR.2015.226
Forward and Backward Bisimulations for Chemical Reaction Networks

Authors: Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
We present two quantitative behavioral equivalences over species of a chemical reaction network (CRN) with semantics based on ordinary differential equations. Forward CRN bisimulation identifies a partition where each equivalence class represents the exact sum of the concentrations of the species belonging to that class. Backward CRN bisimulation relates species that have identical solutions at all time points when starting from the same initial conditions. Both notions can be checked using only CRN syntactical information, i.e., by inspection of the set of reactions. We provide a unified algorithm that computes the coarsest refinement up to our bisimulations in polynomial time. Further, we give algorithms to compute quotient CRNs induced by a bisimulation. As an application, we find significant reductions in a number of models of biological processes from the literature. In two cases we allow the analysis of benchmark models which would be otherwise intractable due to their memory requirements.
Cite as

Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin. Forward and Backward Bisimulations for Chemical Reaction Networks. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 226-239, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cardelli_et_al:LIPIcs.CONCUR.2015.226,
  author =	{Cardelli, Luca and Tribastone, Mirco and Tschaikowski, Max and Vandin, Andrea},
  title =	{{Forward and Backward Bisimulations for Chemical Reaction Networks}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{226--239},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.226},
  URN =		{urn:nbn:de:0030-drops-53684},
  doi =		{10.4230/LIPIcs.CONCUR.2015.226},
  annote =	{Keywords: Chemical reaction networks, ordinary differential equations, bisimulation, partition refinement}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.144
Continuous Markovian Logic - From Complete Axiomatization to the Metric Space of Formulas

Authors: Luca Cardelli, Kim G. Larsen, and Radu Mardare

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
Continuous Markovian Logic (CML) is a multimodal logic that expresses quantitative and qualitative properties of continuous-space and continuous-time labelled Markov processes (CMPs). The modalities of CML approximate the rates of the exponentially distributed random variables that characterize the duration of the labeled transitions. In this paper we present a sound and complete Hilbert-style axiomatization of CML for the CMP-semantics and prove some metaproperties including the small model property. CML characterizes stochastic bisimulation and supports the definition of a quantified extension of satisfiability relation that measures the compatibility of a model and a property. Relying on the small model property, we prove that this measure can be approximated, within a given error, by using a distance between logical formulas.
Cite as

Luca Cardelli, Kim G. Larsen, and Radu Mardare. Continuous Markovian Logic - From Complete Axiomatization to the Metric Space of Formulas. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 144-158, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{cardelli_et_al:LIPIcs.CSL.2011.144,
  author =	{Cardelli, Luca and Larsen, Kim G. and Mardare, Radu},
  title =	{{Continuous Markovian Logic - From Complete Axiomatization to the Metric Space of Formulas}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{144--158},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.144},
  URN =		{urn:nbn:de:0030-drops-32281},
  doi =		{10.4230/LIPIcs.CSL.2011.144},
  annote =	{Keywords: probabilistic logic, axiomatization, Markov processes, metric semantics}
}
Document
DOI: 10.4230/DagSemProc.10271.1
10271 Abstracts Collection – Verification over discrete-continuous boundaries

Authors: Bernd Becker, Luca Cardelli, Holger Hermanns, and Sofiene Tahar

Published in: Dagstuhl Seminar Proceedings, Volume 10271, Verification over discrete-continuous boundaries (2010)

Abstract
From 4 July 2010 to 9 July 2010, the Dagstuhl Seminar 10271 ``Verification over discrete-continuous boundaries'' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Bernd Becker, Luca Cardelli, Holger Hermanns, and Sofiene Tahar. 10271 Abstracts Collection – Verification over discrete-continuous boundaries. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:DagSemProc.10271.1,
  author =	{Becker, Bernd and Cardelli, Luca and Hermanns, Holger and Tahar, Sofiene},
  title =	{{10271 Abstracts Collection – Verification over discrete-continuous boundaries}},
  booktitle =	{Verification over discrete-continuous boundaries},
  pages =	{1--19},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10271},
  editor =	{Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.1},
  URN =		{urn:nbn:de:0030-drops-27922},
  doi =		{10.4230/DagSemProc.10271.1},
  annote =	{Keywords: Formal verification, cyber-physical systems, analog circuits, theorem proving, systems biology, mean-field methods}
}
Document
DOI: 10.4230/DagSemProc.10271.2
A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra

Authors: Erika Abraham, Florian Corzilius, Ulrich Loup, and Thomas Sturm

Published in: Dagstuhl Seminar Proceedings, Volume 10271, Verification over discrete-continuous boundaries (2010)

Abstract
There are several methods for the synthesis and analysis of hybrid systems that require efficient algorithms and tools for satisfiability checking. For analysis, e.g., bounded model checking describes counterexamples of a fixed length by logical formulas, whose satisfiability corresponds to the existence of such a counterexample. As an example for parameter synthesis, we can state the correctness of a parameterized system by a logical formula; the solution set of the formula gives us possible safe instances of the parameters. For discrete systems, which can be described by propositional logic formulas, SAT-solvers can be used for the satisfiability checks. For hybrid systems, having mixed discrete-continuous behavior, SMT-solvers are needed. SMT-solving extends SAT with theories, and has its main focus on linear arithmetic, which is sufficient to handle, e.g., linear hybrid systems. However, there are only few solvers for more expressive but still decidable logics like the first-order theory of the reals with addition and multiplication -- real algebra. Since the synthesis and analysis of non-linear hybrid systems requires such a powerful logic, we need efficient SMT-solvers for real algebra. Our goal is to develop such an SMT-solver for the real algebra, which is both complete and efficient.
Cite as

Erika Abraham, Florian Corzilius, Ulrich Loup, and Thomas Sturm. A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{abraham_et_al:DagSemProc.10271.2,
  author =	{Abraham, Erika and Corzilius, Florian and Loup, Ulrich and Sturm, Thomas},
  title =	{{A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra}},
  booktitle =	{Verification over discrete-continuous boundaries},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10271},
  editor =	{Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.2},
  URN =		{urn:nbn:de:0030-drops-27907},
  doi =		{10.4230/DagSemProc.10271.2},
  annote =	{Keywords: SMT-solving, Real Algebra, Hybrid Systems, Verification, Synthesis}
}
Document
DOI: 10.4230/DagSemProc.10271.3
Network-driven Boolean Normal Forms

Authors: Michael Brickenstein and Alexander Dreyer

Published in: Dagstuhl Seminar Proceedings, Volume 10271, Verification over discrete-continuous boundaries (2010)

Abstract
We apply the PolyBoRi framework for Groebner bases computations with Boolean polynomials to bit-valued problems from algebraic cryptanalysis and formal verification. First, we proposed zero-suppressed binary decision diagrams (ZDDs) as a suitable data structure for Boolean polynomials. Utilizing the advantages of ZDDs we develop new reduced normal form algorithms for linear lexicographical lead rewriting systems. The latter play an important role in modeling bit-valued components of digital systems. Next, we reorder the variables in Boolean polynomial rings with respect to the topology of digital components. This brings computational algebra to digital circuits and small scale crypto systems in the first place. We additionally propose an optimized topological ordering, which tends to keep the intermediate results small. Thus, we successfully applied the linear lexicographical lead techniques to non-trivial examples from formal verification of digital systems. Finally, we evaluate the performance using benchmark examples from formal verification and cryptanalysis including equivalence checking of a bit-level formulation of multiplier components. Before we introduced topological orderings in PolyBoRi, state of the art for the algebraic approach was a bit-width of 4 for each factor. By combining our techniques we raised this bound to 16, which is an important step towards real-world applications.
Cite as

Michael Brickenstein and Alexander Dreyer. Network-driven Boolean Normal Forms. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{brickenstein_et_al:DagSemProc.10271.3,
  author =	{Brickenstein, Michael and Dreyer, Alexander},
  title =	{{Network-driven Boolean Normal Forms}},
  booktitle =	{Verification over discrete-continuous boundaries},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10271},
  editor =	{Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.3},
  URN =		{urn:nbn:de:0030-drops-27894},
  doi =		{10.4230/DagSemProc.10271.3},
  annote =	{Keywords: Groebner, normal forms, Boolean polynomials, cryptanalysis, verification}
}
Document
DOI: 10.4230/DagSemProc.10271.4
Towards more Dependable Verification of Mixed-Signal Systems

Authors: Florian Schupfer and Christoph Grimm

Published in: Dagstuhl Seminar Proceedings, Volume 10271, Verification over discrete-continuous boundaries (2010)

Abstract
The verification of complex mixed-signal systems is a challenge, especially considering the impact of parameter variations. Besides the established approaches like Monte-Carlo or Corner-Case simulation, a novel semi-symbolic approach emerged in recent years. In this approach, parameter variations and tolerances are maintained as symbolic ranges during numerical simulation runs by using affine arithmetic. Maintaining parameter variations and tolerances in a symbolic way significantly increases verification coverage. In the following we give a brief introduction and an overview of research on semi-symbolic simulation of both circuits and systems and discuss possible application for system level verification and optimization.
Cite as

Florian Schupfer and Christoph Grimm. Towards more Dependable Verification of Mixed-Signal Systems. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{schupfer_et_al:DagSemProc.10271.4,
  author =	{Schupfer, Florian and Grimm, Christoph},
  title =	{{Towards more Dependable Verification of Mixed-Signal Systems}},
  booktitle =	{Verification over discrete-continuous boundaries},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10271},
  editor =	{Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.4},
  URN =		{urn:nbn:de:0030-drops-27911},
  doi =		{10.4230/DagSemProc.10271.4},
  annote =	{Keywords: Affine Arithmetic, Range based methods, Verification, Semi-symbolic simulation}
}
Document
DOI: 10.4230/DagSemRep.216
The Semantic Challenge of Object-Oriented Programming (Dagstuhl Seminar 98261)

Authors: Luca Cardelli, Achim Jung, Peter O'Hearn, and Jens Palsberg

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Luca Cardelli, Achim Jung, Peter O'Hearn, and Jens Palsberg. The Semantic Challenge of Object-Oriented Programming (Dagstuhl Seminar 98261). Dagstuhl Seminar Report 216, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1999)

Copy BibTex To Clipboard

@TechReport{cardelli_et_al:DagSemRep.216,
  author =	{Cardelli, Luca and Jung, Achim and O'Hearn, Peter and Palsberg, Jens},
  title =	{{The Semantic Challenge of Object-Oriented Programming (Dagstuhl Seminar 98261)}},
  pages =	{1--14},
  ISSN =	{1619-0203},
  year =	{1999},
  type = 	{Dagstuhl Seminar Report},
  number =	{216},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.216},
  URN =		{urn:nbn:de:0030-drops-151022},
  doi =		{10.4230/DagSemRep.216},
}
  • Refine by Author
  • 4 Cardelli, Luca
  • 1 Abraham, Erika
  • 1 Becker, Bernd
  • 1 Brickenstein, Michael
  • 1 Corzilius, Florian
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 Verification
  • 1 Affine Arithmetic
  • 1 Boolean polynomials
  • 1 Chemical reaction networks
  • 1 Formal verification
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 4 2010
  • 1 1999
  • 1 2011
  • 1 2015

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact