-
B. Lacerda,
F. Faruq,
D. Parker,
and N. Hawes.
Probabilistic Planning with Formal Performance Guarantees for Mobile Service Robots.
International Journal of Robotics Research,
38(19):1098-1123,
2019.
Keyword(s): model checking,
probability.
@article{lacerdaProbabilisticPlanningFormal2019,
title = {Probabilistic Planning with Formal Performance Guarantees for Mobile Service Robots},
author = {Lacerda, B. and Faruq, F. and Parker, D. and Hawes, N.},
year = {2019},
volume = {38},
pages = {1098--1123},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4351-Lacerda et al (2019) - Probabilistic planning with formal performance guarantees for mobile service.pdf},
journal = {International Journal of Robotics Research},
keywords = {model checking,probability},
number = {19}
}
-
Changliu Liu,
Tomer Arnon,
Christopher Lazarus,
Clark Barrett,
and Mykel J. Kochenderfer.
Algorithms for Verifying Deep Neural Networks.
arXiv:1903.06758 [cs, stat],
March 2019.
Keyword(s): model checking.
Abstract: |
Deep neural networks are widely used for nonlinear function approximation with applications ranging from computer vision to control. Although these networks involve the composition of simple arithmetic operations, it can be very challenging to verify whether a particular network satisfies certain input-output properties. This article surveys methods that have emerged recently for soundly verifying such properties. These methods borrow insights from reachability analysis, optimization, and search. We discuss fundamental differences and connections between existing algorithms. In addition, we provide pedagogical implementations of existing methods and compare them on a set of benchmark problems. |
@article{liuAlgorithmsVerifyingDeep2019,
title = {Algorithms for {{Verifying Deep Neural Networks}}},
author = {Liu, Changliu and Arnon, Tomer and Lazarus, Christopher and Barrett, Clark and Kochenderfer, Mykel J.},
year = {2019},
month = mar,
abstract = {Deep neural networks are widely used for nonlinear function approximation with applications ranging from computer vision to control. Although these networks involve the composition of simple arithmetic operations, it can be very challenging to verify whether a particular network satisfies certain input-output properties. This article surveys methods that have emerged recently for soundly verifying such properties. These methods borrow insights from reachability analysis, optimization, and search. We discuss fundamental differences and connections between existing algorithms. In addition, we provide pedagogical implementations of existing methods and compare them on a set of benchmark problems.},
archivePrefix = {arXiv},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4284-Liu et al (2019) - Algorithms for Verifying Deep Neural Networks.pdf},
journal = {arXiv:1903.06758 [cs, stat]},
keywords = {model checking},
}
-
C. Faggian and S. R. d Rocca.
Lambda Calculus and Probabilistic Computation.
In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS),
pages 1-13,
June 2019.
Keyword(s): calculus,
probability.
Abstract: |
We introduce two extensions of the {$\lambda$} -calculus with a probabilistic choice operator, {$\Lambda\oplus$}cbv and {$\Lambda\oplus$}cbn, modeling respectively call-by-value and call-by-name probabilistic computation. We prove that both enjoys confluence and standardization, in an extended way: we revisit these two fundamental notions to take into account the asymptotic behaviour of terms. The common root of the two calculi is a further calculus based on Linear Logic, {$\Lambda\oplus$}!, which allows us to develop a unified, modular approach. |
@inproceedings{faggianLambdaCalculusProbabilistic2019,
title = {Lambda {{Calculus}} and {{Probabilistic Computation}}},
booktitle = {2019 34th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}} ({{LICS}})},
author = {Faggian, C. and d Rocca, S. R.},
year = {2019},
month = jun,
pages = {1--13},
doi = {10.1109/LICS.2019.8785699},
abstract = {We introduce two extensions of the {$\lambda$} -calculus with a probabilistic choice operator, {$\Lambda\oplus$}cbv and {$\Lambda\oplus$}cbn, modeling respectively call-by-value and call-by-name probabilistic computation. We prove that both enjoys confluence and standardization, in an extended way: we revisit these two fundamental notions to take into account the asymptotic behaviour of terms. The common root of the two calculi is a further calculus based on Linear Logic, {$\Lambda\oplus$}!, which allows us to develop a unified, modular approach.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4768-Faggian_Rocca (2019) - Lambda Calculus and Probabilistic Computation.pdf},
keywords = {calculus,probability}
}
-
M. Kwiatkowska,
G. Norman,
and D. Parker.
Verification and Control of Turn-Based Probabilistic Real-Time Games.
In M. Alvim,
K. Chatzikokolakis,
C. Olarte,
and F. Valencia, editors,
The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy (Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday),
volume 11760 of LNCS,
pages 379-396,
2019.
Springer.
Keyword(s): model checking,
probability.
@inproceedings{kwiatkowskaVerificationControlTurnBased2019,
title = {Verification and {{Control}} of {{Turn}}-{{Based Probabilistic Real}}-{{Time Games}}},
booktitle = {The {{Art}} of {{Modelling Computational Systems}}: {{A Journey}} from {{Logic}} and {{Concurrency}} to {{Security}} and {{Privacy}} ({{Essays Dedicated}} to {{Catuscia Palamidessi}} on the {{Occasion}} of {{Her}} 60th {{Birthday}})},
author = {Kwiatkowska, M. and Norman, G. and Parker, D.},
editor = {Alvim, M. and Chatzikokolakis, K. and Olarte, C. and Valencia, F.},
year = {2019},
volume = {11760},
pages = {379--396},
publisher = {{Springer}},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4353-Kwiatkowska et al (2019) - Verification and Control of Turn-Based Probabilistic Real-Time Games.pdf},
keywords = {model checking,probability},
series = {{{LNCS}}}
}
-
Wenbo Zhang,
Huan Long,
and Xian Xu.
Uniform Random Process Model Revisited.
In Anthony Widjaja Lin, editor,
Programming Languages and Systems,
Lecture Notes in Computer Science,
Cham,
pages 388-404,
2019.
Springer International Publishing.
ISBN: 978-3-030-34175-6.
Keyword(s): pi calculus,
calculus,
probability.
Abstract: |
Recently, a proper bisimulation equivalence relation for random process model has been defined in a model independent approach. Model independence clarifies the difference between nondeterministic and probabilistic actions in concurrency and makes the new equivalence relation to be congruent. In this paper, we focus on the finite state randomized CCS model and deepen the previous work in two aspects. First, we show that the equivalence relation can be decided in polynomial time. Second, we give a sound and complete axiomatization system for this model. The algorithm and axiomatization system also have the merit of model independency as they can be easily generalized to the randomized extension of any finite state concurrent model. |
@inproceedings{zhangUniformRandomProcess2019,
title = {Uniform {{Random Process Model Revisited}}},
booktitle = {Programming {{Languages}} and {{Systems}}},
author = {Zhang, Wenbo and Long, Huan and Xu, Xian},
editor = {Lin, Anthony Widjaja},
year = {2019},
pages = {388--404},
publisher = {{Springer International Publishing}},
address = {{Cham}},
doi = {10.1007/978-3-030-34175-6_20},
abstract = {Recently, a proper bisimulation equivalence relation for random process model has been defined in a model independent approach. Model independence clarifies the difference between nondeterministic and probabilistic actions in concurrency and makes the new equivalence relation to be congruent. In this paper, we focus on the finite state randomized CCS model and deepen the previous work in two aspects. First, we show that the equivalence relation can be decided in polynomial time. Second, we give a sound and complete axiomatization system for this model. The algorithm and axiomatization system also have the merit of model independency as they can be easily generalized to the randomized extension of any finite state concurrent model.},
isbn = {978-3-030-34175-6},
series = {Lecture {{Notes}} in {{Computer Science}}},
keywords = {pi calculus,calculus,probability},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4773-Zhang et al (2019) - Uniform Random Process Model Revisited.pdf}
}
-
Donnacha Oisìn Kidney.
Probability Monads in Cubical Agda.
https://doisinkidney.com/posts/2019-04-17-cubical-probability.html,
April 2019.
Keyword(s): probability.
@misc{kidneyProbabilityMonadsCubical2019,
title = {Probability {{Monads}} in {{Cubical Agda}}},
author = {Kidney, Donnacha Ois{\'i}n},
year = {2019},
month = apr,
howpublished = {https://doisinkidney.com/posts/2019-04-17-cubical-probability.html},
keywords = {probability},
}
-
Reynald Affeldt,
Jacques Garrigue,
and Takafumi Saikawa.
Reasoning with Conditional Probabilities and Joint Distributions in Coq.
,
March 2019.
Keyword(s): Coq,
probability.
Abstract: |
Probabilities occur in many applications of computer science, such as communication theory and artificial intelligence. These are critical applications that require some form of verification to guarantee the quality of their implementations. Unfortunately, probabilities are also the typical example of a mathematical theory whose abuses of notations make pencil-and-paper proofs difficult to formalize. In this paper, we experiment a new formalization of conditional probabilities that we validate with two applications. First, we formalize the foundational definitions and theorems of information theory, extending previous work with new lemmas. Second, we formalize the notion of conditional independence and its properties, paving the road for a formalization of graphical probabilistic models. |
@unpublished{affeldtReasoningConditionalProbabilities2019,
title = {Reasoning with {{Conditional Probabilities}} and {{Joint Distributions}} in {{Coq}}},
author = {Affeldt, Reynald and Garrigue, Jacques and Saikawa, Takafumi},
year = {2019},
month = mar,
address = {{21st Workshop on Programming and Programming Languages (PPL2019). Japan Society for Software Science and Technology, Iwate-ken, Hanamaki-shi}},
abstract = {Probabilities occur in many applications of computer science, such as communication theory and artificial intelligence. These are critical applications that require some form of verification to guarantee the quality of their implementations. Unfortunately, probabilities are also the typical example of a mathematical theory whose abuses of notations make pencil-and-paper proofs difficult to formalize. In this paper, we experiment a new formalization of conditional probabilities that we validate with two applications. First, we formalize the foundational definitions and theorems of information theory, extending previous work with new lemmas. Second, we formalize the notion of conditional independence and its properties, paving the road for a formalization of graphical probabilistic models.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4206-Affeldt et al (2019) - Reasoning with Conditional Probabilities and Joint Distributions in Coq.pdf},
keywords = {Coq,probability},
}