1biblio_conf.bib

@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bib2bib -c 1=1 /home/pedro/git/private//papers/conferencias.bib}}
@inproceedings{DWTC09:qest,
  author = {D'Argenio, Pedro R. and  Wolovick, Nicol\'as and S{\'a}nchez Terraf, Pedro  and  Celayes, Pablo},
  title = {Nondeterministic Labeled {M}arkov Processes: Bisimulations
               and Logical Characterization},
  publisher = {IEEE Computer Society},
  booktitle = {QEST, Sixth International Conference on the Quantitative Evaluation of Systems},
  year = 2009,
  pages = {11--20},
  zbl = {1426.68188},
  doi = {10.1109/QEST.2009.17},
  ee = {http://doi.ieeecomputersociety.org/10.1109/QEST.2009.17},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@incollection{ROCKS,
  year = 2014,
  isbn = {978-3-662-45488-6},
  booktitle = {Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems},
  volume = 8453,
  series = {Lecture Notes in Computer Science},
  editor = {Remke, Anne and Stoelinga, Mariëlle},
  doi = {10.1007/978-3-662-45489-3\_3},
  title = {A Theory for the Semantics of Stochastic and Non-deterministic Continuous Systems},
  url = {http://dx.doi.org/10.1007/978-3-662-45489-3_3},
  publisher = {Springer Berlin Heidelberg},
  pages = {67-86},
  language = {English},
  author = { Budde, Carlos E. and D'Argenio, Pedro R. and S{\'a}nchez Terraf, Pedro and Wolovick, Nicol\'as},
  abstract = {The description of complex systems involving physical or biological components usually requires to model involved continuous behavior induced by variables such as time, distances, speed, temperature, alkalinity of a solution, etc. Often, such variables can be quantified probabilistically to better understand the behavior of the complex systems. For example, the arrival time of events may be considered a Poisson process or the weight of an individual may be assumed to be distributed according to a log-normal distribution. However, it is also common that the uncertainty on how these variables behave make us prefer to leave out the choice of a particular probability and rather model it as a purely non-deterministic decision, as it is the case when a system is intended to be deployed in a variety of very different computer or network architectures. Therefore, the semantics of these systems needs to be represented by a variant of probabilistic automata that involves continuous domains on the state space and the transition relation.
In this paper, we provide a survey to the theory of such kind of models. We present the theory of the so called labeled Markov processes (LMP) and its extension with internal non-determinism (NLMP). We show that in these complex domains, the bisimulation relation can be understood in different manners. We show the relation among these different definitions and try to understand the boundaries among them through examples. We also study variants of Hennessy-Milner logic that provides logical characterizations of some of these bisimulations.}
}
@article{2018arXiv180705174G,
  author = {Gunther, Emmanuel and Pagano, Miguel and S{\'a}nchez Terraf, Pedro},
  title = {{First steps towards a formalization of Forcing}},
  journal = {Electronic Notes in Theoretical Computer Science},
  archiveprefix = {arXiv},
  eprint = {1807.05174},
  primaryclass = {cs.LO},
  keywords = {Computer Science - Logic in Computer Science, 03B35 (Primary) 03E40, 03B70, 68T15 (Secondary), F.4.1},
  month = jul,
  adsurl = {http://adsabs.harvard.edu/abs/2018arXiv180705174G},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System},
  abstract = {We lay the ground for an Isabelle/ZF formalization of Cohen's 
  technique of \emph{forcing}. We formalize the definition of forcing notions as
  preorders with top, dense subsets, and generic filters. We formalize
  a version of the principle of Dependent Choices and using it
  we prove the Rasiowa-Sikorski lemma on the existence of generic filters.
  
  Given a transitive set $M$, we define its generic extension $M[G]$,
  the canonical names for elements of $M$, and finally show that if $M$
  satisfies the axiom of pairing, then $M[G]$ also does.},
  volume = {344},
  pages = {119 - 136},
  year = {2019},
  issn = {1571-0661},
  doi = {10.1016/j.entcs.2019.07.008},
  url = {http://www.sciencedirect.com/science/article/pii/S157106611930026X},
  note = {The proceedings of LSFA 2018, the 13th Workshop on Logical and Semantic Frameworks with Applications (LSFA’18)}
}
@inproceedings{2020arXiv200109715G,
  author = {Gunther, Emmanuel and Pagano, Miguel and S{\'a}nchez Terraf, Pedro},
  title = {{Formalization of Forcing in Isabelle/ZF}},
  isbn = {978-3-662-45488-6},
  booktitle = {Automated Reasoning. 10th International Joint Conference, IJCAR 2020, Paris, France, July 1--4, 2020, Proceedings, Part II},
  volume = 12167,
  series = {Lecture Notes in Artificial Intelligence},
  editor = {Peltier, Nicolas and  Sofronie-Stokkermans, Viorica},
  publisher = {Springer International Publishing},
  doi = {10.1007/978-3-030-51054-1},
  pages = {221--235},
  journal = {arXiv e-prints},
  keywords = {Computer Science - Logic in Computer Science, Mathematics - Logic, 03B35 (Primary) 03E40, 03B70, 68T15 (Secondary), F.4.1},
  year = 2020,
  archiveprefix = {arXiv},
  eprint = {2001.09715},
  primaryclass = {cs.LO},
  adsurl = {https://ui.adsabs.harvard.edu/abs/2020arXiv200109715G},
  abstract = {We formalize the theory of forcing in the set theory framework of
Isabelle/ZF. Under the assumption of the existence of a countable
transitive model of $\mathit{ZFC}$, we construct a proper generic extension and show
that the latter also satisfies $\mathit{ZFC}$. In doing so, we remodularized
Paulson's ZF-Constructibility library.},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

This file was generated by bibtex2html 1.99.